Changeset 1238 for src/Clight/test/search.c.ma

Timestamp:

Sep 21, 2011, 4:25:36 PM (9 years ago)

Author:

campbell

Message:

Update Cminor and RTLabs to fit SmallstepExec? changes.

File:

• src/Clight/test/search.c.ma (modified) (2 diffs)

src/Clight/test/search.c.ma

@@ -192 +192 @@
 include "Cminor/semantics.ma".
 
+example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
+(*
 example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
+*)
 normalize
 @refl
@@ -202 +205 @@
 example e2: finishes_with (repr 3) ? (
 do p1 ← clight_to_cminor myprog;
+bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2.
+ exec_up_to RTLabs_fullexec p2 1000 [ ])).
+(*
+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 [ ]).
+ exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
 normalize
 @refl