source: src/Clight/test/goto-if.test.ma @ 2253

Last change on this file since 2253 was 2253, checked in by campbell, 7 years ago

Cminor to RTLabs is now a total function.

File size: 1.1 KB
Line 
1include "Clight/test/goto-if.c.ma".
2
3example exec: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
4normalize  (* you can examine the result here *)
5%
6qed.
7
8include "Clight/label.ma".
9
10definition myprog' ≝ clight_label myprog.
11
12example el: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog' 1000 [ ]).
13normalize  (* you can examine the result here *)
14%
15qed.
16
17include "Clight/SimplifyCasts.ma".
18
19example es: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec (simplify_program myprog') 1000 [ ]).
20normalize  (* you can examine the result here *)
21%
22qed.
23
24include "Clight/toCminor.ma".
25include "Cminor/semantics.ma".
26
27example e1: finishes_with (repr I32 0) ?
28  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog'))
29   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
30normalize
31%
32qed.
33
34include "Cminor/toRTLabs.ma".
35include "RTLabs/semantics.ma".
36
37example e2: finishes_with (repr I32 0) ? (
38bind ? (snapshot state) (clight_to_cminor (simplify_program myprog'))
39(λp1. let p2 ≝ cminor_to_rtlabs p1 in
40  exec_up_to RTLabs_fullexec p2 1000 [ ])).
41normalize
42%
43qed.
Note: See TracBrowser for help on using the repository browser.