Changeset 2253 for src/Clight/test/goto-if.test.ma

Timestamp:

Jul 24, 2012, 7:40:22 PM (9 years ago)

Author:

campbell

Message:

Cminor to RTLabs is now a total function.

File:

• src/Clight/test/goto-if.test.ma (modified) (1 diff)

src/Clight/test/goto-if.test.ma

@@ -37 +37 @@
 example e2: finishes_with (repr I32 0) ? (
 bind ? (snapshot state) (clight_to_cminor (simplify_program myprog'))
-(λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
- (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
+(λp1. let p2 ≝ cminor_to_rtlabs p1 in
+  exec_up_to RTLabs_fullexec p2 1000 [ ])).
 normalize
 %