Changeset 2971

Timestamp:

Mar 27, 2013, 11:41:51 AM (7 years ago)

Author:

campbell

Message:

Single RTLabs return statement.

File:

• src/Cminor/toRTLabs.ma (modified) (3 diffs)

src/Cminor/toRTLabs.ma

@@ -636 +636 @@
 
 (* Return statements need a little careful treatment to avoid errors using the
-   invariant about the return type. *)
+   invariant about the return type.  Note that there is one unique return
+   statement at the function's exit. *)
 
 definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
@@ -642 +643 @@
 λfx,opt_e,f.
   let f0 ≝ f in
-  let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
+  let f ≝ change_entry … f (pf_exit … f) (pi2 ???) in
   match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
   [ None ⇒ λEnv. «pi1 … f, ?»
@@ -667 +668 @@
 | @(si_vars … (π1 Env))
 | inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
-| #l #H @I
-| #l //
 ] qed.