source: Deliverables/D3.3/id-lookup-branch/Cminor/test/search.test.ma @ 2113

Last change on this file since 2113 was 1311, checked in by campbell, 10 years ago

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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