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

Last change on this file since 1513 was 1513, checked in by campbell, 9 years ago

Fix up Clight examples.

File size: 889 bytes
Line 
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 *)
6@refl qed.
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 *)
10@refl qed.
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 *)
14@refl qed.
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 *)
18@refl qed.
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 *)
22@refl qed.
Note: See TracBrowser for help on using the repository browser.