Changeset 771 for src/Cminor/test


Ignore:
Timestamp:
Apr 22, 2011, 3:21:28 PM (9 years ago)
Author:
campbell
Message:

Implement switch statements in Cminor -> RTLabs phase

File:
1 edited

Legend:

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

    r770 r771  
    134134include "RTLabs/semantics.ma".
    135135
    136 (* matita translation doesn't do switch yet
    137136example execRTL0: finishes_with (repr 16) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 0)]).
    138137normalize  (* you can examine the result here *)
    139138@refl
    140139qed.
    141 *)
     140
     141example execRTL1: finishes_with (repr 0) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 1)]).
     142normalize  (* you can examine the result here *)
     143@refl
     144qed.
     145
     146example execRTL3: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 3)]).
     147normalize  (* you can examine the result here *)
     148@refl
     149qed.
     150
     151example execRTL5: finishes_with (repr 5) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 5)]).
     152normalize  (* you can examine the result here *)
     153@refl
     154qed.
     155
     156example execRTL7: finishes_with (repr 3) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 7)]).
     157normalize  (* you can examine the result here *)
     158@refl
     159qed.
Note: See TracChangeset for help on using the changeset viewer.