Changeset 1311 for Deliverables/D3.3/id-lookup-branch/Cminor/test

Timestamp:

Oct 6, 2011, 6:45:54 PM (8 years ago)

Author:

campbell

Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• Cminor/test/search.Cminor.ma (modified) (2 diffs)
• Cminor/test/search.test.ma (copied) (copied from src/Cminor/test/search.test.ma)

Deliverables/D3.3/id-lookup-branch/Cminor/test/search.Cminor.ma

@@ -281 +281 @@
 
 definition myprog : Cminor_program :=
-mk_program ?? [
+mk_program ?? [] [
   (pair ?? id__div32u f__div32u);
   (pair ?? id__div32s f__div32s);
@@ -287 +287 @@
   (pair ?? id_main f_main)
 ]  id_main
-[]
 .
-
-   example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
-   normalize  (* you can examine the result here *)
-   @refl qed.
-
-
-include "Cminor/toRTLabs.ma".
-include "RTLabs/semantics.ma".
-
-example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
-normalize  (* you can examine the result here *)
-@refl
-qed.
-
-