source: src/Clight/test/sum.test.ma @ 1226

Last change on this file since 1226 was 1226, checked in by campbell, 8 years ago

Adjust pretty printers for change in program records, try a test of each.

File size: 862 bytes
Line 
1include "Clight/test/sum.c.ma".
2
3example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
4normalize  (* you can examine the result here *)
5@refl
6qed.
7
8include "Clight/SimplifyCasts.ma".
9
10example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
11normalize  (* you can examine the result here *)
12@refl
13qed.
14
15include "Clight/toCminor.ma".
16include "Cminor/semantics.ma".
17
18example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]).
19normalize
20@refl
21qed.
22
23include "Cminor/toRTLabs.ma".
24include "RTLabs/semantics.ma".
25
26example e2: finishes_with (repr I32 74) ? (
27do p1 ← clight_to_cminor (simplify_program myprog);
28do p2 ← cminor_to_rtlabs p1;
29 exec_up_to RTLabs_fullexec p2 1000 [ ]).
30normalize
31@refl
32qed.
Note: See TracBrowser for help on using the repository browser.