Changeset 1883


Ignore:
Timestamp:
Apr 9, 2012, 11:53:35 AM (8 years ago)
Author:
campbell
Message:

Ilias' switch removal code, plus a test.

Location:
src/Clight
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/switcher.test.ma

    r1876 r1883  
    2121normalize  (* you can examine the result here *)
    2222% qed.
     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 TracChangeset for help on using the changeset viewer.