Ignore:
Timestamp:
Apr 22, 2011, 1:49:12 PM (10 years ago)
Author:
campbell
Message:

Make Cminor tests test translation to RTLabs.

File:
1 edited

Legend:

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

    r751 r768  
    7777normalize  (* you can examine the result here *)
    7878@refl qed.
     79
     80include "Cminor/toRTLabs.ma".
     81include "RTLabs/semantics.ma".
     82
     83example execRTL: finishes_with (repr 120) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 5)]).
     84normalize  (* you can examine the result here *)
     85@refl
     86qed.
     87
Note: See TracChangeset for help on using the changeset viewer.