Changeset 731 for src/Clight/test/search.ma

Timestamp:

Apr 1, 2011, 1:35:18 PM (10 years ago)

Author:

campbell

Message:

Common definition for animation semantics, and factor out IO definitions.

File:

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

src/Clight/test/search.ma

@@ -1 @@
-include "Clight/Animation.ma".
+include "Clight/Cexec.ma".
+include "common/Animation.ma".
 
 definition myprog := mk_program clight_fundef type
@@ -188 +189 @@
 .
 
-example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).
+example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
 normalize  (* you can examine the result here *)
 %