Changeset 816 for src/Clight/test

Timestamp:

May 19, 2011, 3:06:42 PM (10 years ago)

Author:

campbell

Message:

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

File:

• src/Clight/test/search.ma (modified) (1 diff)

src/Clight/test/search.ma

@@ -193 +193 @@
 @refl
 qed.
+
+include "Clight/toCminor.ma".
+include "Cminor/semantics.ma".
+
+example e1: finishes_with (repr 3) ? (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 3) ? (
+do p1 ← clight_to_cminor myprog;
+do p2 ← cminor_to_rtlabs p1;
+ exec_up_to RTLabs_fullexec p2 1000 [ ]).
+normalize
+@refl
+qed.