Changeset 881 for src/Clight/test/io.ma

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.

File:

• src/Clight/test/io.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.