source: src/Cminor/test/null-op.test.ma @ 1971

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

Update Cminor pretty printer and examples.

File size: 470 bytes
Line 
1include "Cminor/test/null-op.Cminor.ma".
2
3example exec: finishes_with (repr I32 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
4normalize  (* you can examine the result here *)
5@refl
6qed.
7
8include "Cminor/toRTLabs.ma".
9include "RTLabs/semantics.ma".
10
11example execRTL: finishes_with (repr 1) ?
12 (bind ? (snapshot state) (cminor_to_rtlabs myprog)
13  (λmyprog'. exec_up_to RTLabs_fullexec myprog' 1000 [ ])).
14normalize  (* you can examine the result here *)
15@refl
16qed.
17
Note: See TracBrowser for help on using the repository browser.