source: src/Clight/test/switcher.test.ma

Last change on this file was 1883, checked in by campbell, 8 years ago

Ilias' switch removal code, plus a test.

File size: 1.8 KB
RevLine 
[1513]1include "Clight/test/switcher.c.ma".
2
3
4example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]).
5normalize  (* you can examine the result here *)
[1876]6% qed.
[1513]7
8example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]).
9normalize  (* you can examine the result here *)
[1876]10% qed.
[1513]11
12example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]).
13normalize  (* you can examine the result here *)
[1876]14% qed.
[1513]15
16example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
17normalize  (* you can examine the result here *)
[1876]18% qed.
[1513]19
20example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]).
21normalize  (* you can examine the result here *)
[1876]22% qed.
[1883]23
24include "Clight/switchRemoval.ma".
25
26definition noswitch ≝ program_switch_removal myprog.
27
28example exec0': finishes_with (repr I32 16) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 0)]).
29normalize  (* you can examine the result here *)
30% qed.
31
32example exec1': finishes_with (repr I32 0) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 1)]).
33normalize  (* you can examine the result here *)
34% qed.
35
36example exec3': finishes_with (repr I32 1) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 3)]).
37normalize  (* you can examine the result here *)
38% qed.
39
40example exec5': finishes_with (repr I32 5) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 5)]).
41normalize  (* you can examine the result here *)
42% qed.
43
44example exec7': finishes_with (repr I32 3) ? (exec_up_to clight_fullexec noswitch 1000 [EVint I32 (repr ? 7)]).
45normalize  (* you can examine the result here *)
46% qed.
Note: See TracBrowser for help on using the repository browser.