Changeset 1883 for src/Clight/test

Timestamp:

Apr 9, 2012, 11:53:35 AM (9 years ago)

Author:

campbell

Message:

Ilias' switch removal code, plus a test.

File:

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

src/Clight/test/switcher.test.ma

@@ -21 +21 @@
 normalize  (* you can examine the result here *)
 % qed.
+
+include "Clight/switchRemoval.ma".
+
+definition noswitch ≝ program_switch_removal myprog.
+
+example exec0': finishes_with (repr I32 16) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 0)]).
+normalize  (* you can examine the result here *)
+% qed.
+
+example exec1': finishes_with (repr I32 0) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 1)]).
+normalize  (* you can examine the result here *)
+% qed.
+
+example exec3': finishes_with (repr I32 1) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 3)]).
+normalize  (* you can examine the result here *)
+% qed.
+
+example exec5': finishes_with (repr I32 5) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 5)]).
+normalize  (* you can examine the result here *)
+% qed.
+
+example exec7': finishes_with (repr I32 3) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 7)]).
+normalize  (* you can examine the result here *)
+% qed.