| Rev | Line | |
|---|
| [1513] | 1 | include "Clight/test/switcher.c.ma". |
|---|
| 2 | |
|---|
| 3 | |
|---|
| 4 | example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]). |
|---|
| 5 | normalize (* you can examine the result here *) |
|---|
| 6 | @refl qed. |
|---|
| 7 | |
|---|
| 8 | example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]). |
|---|
| 9 | normalize (* you can examine the result here *) |
|---|
| 10 | @refl qed. |
|---|
| 11 | |
|---|
| 12 | example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]). |
|---|
| 13 | normalize (* you can examine the result here *) |
|---|
| 14 | @refl qed. |
|---|
| 15 | |
|---|
| 16 | example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]). |
|---|
| 17 | normalize (* you can examine the result here *) |
|---|
| 18 | @refl qed. |
|---|
| 19 | |
|---|
| 20 | example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]). |
|---|
| 21 | normalize (* you can examine the result here *) |
|---|
| 22 | @refl qed. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
