Changeset 881 for src/Clight/test

Timestamp:

Jun 3, 2011, 5:35:31 PM (10 years ago)

Author:

campbell

Message:

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

Location:

src/Clight/test

Files:

• io.ma (modified) (1 diff)
• sum.ma (modified) (1 diff)

src/Clight/test/io.ma

@@ -28 +28 @@
 @refl
 qed.
+
+
+include "Clight/toCminor.ma".
+include "Cminor/semantics.ma".
+
+example e1: (do p ← clight_to_cminor myprog;
+             do r ← exec_up_to Cminor_fullexec p 1000 [EVint (repr 7) ];
+             match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
+ OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
+normalize
+@refl
+qed.
+
+include "Cminor/toRTLabs.ma".
+include "RTLabs/semantics.ma".
+
+example e2: (do p1 ← clight_to_cminor myprog;
+             do p2 ← cminor_to_rtlabs p1;
+             do r ← exec_up_to RTLabs_fullexec p2 1000 [EVint (repr 7) ];
+             match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
+ OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
+normalize
+@refl
+qed.

src/Clight/test/sum.ma

@@ -60 +60 @@
 @refl
 qed.
+
+include "Clight/toCminor.ma".
+include "Cminor/semantics.ma".
+
+example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
+normalize
+@refl
+qed.
+
+include "Cminor/toRTLabs.ma".
+include "RTLabs/semantics.ma".
+
+example e2: finishes_with (repr 74) ? (
+do p1 ← clight_to_cminor myprog;
+do p2 ← cminor_to_rtlabs p1;
+ exec_up_to RTLabs_fullexec p2 1000 [ ]).
+normalize
+@refl
+qed.