source: src/Clight/test/search.test.ma @ 1991

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

Put the front end transformations together and make an example use it.

File size: 1.0 KB
Line 
1include "compiler.ma".
2include "common/Animation.ma".
3include "Clight/test/search.c.ma".
4
5(* Check the original works. *)
6
7example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
8normalize  (* you can examine the result here *)
9%
10qed.
11
12(* Check some individual passes. *)
13
14include "Cminor/semantics.ma".
15
16example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
17normalize
18%
19qed.
20
21include "RTLabs/semantics.ma".
22
23example e2: finishes_with (repr 3) ? (
24do p1 ← clight_to_cminor myprog;
25bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2.
26 exec_up_to RTLabs_fullexec p2 1000 [ ])).
27(*
28example e2: finishes_with (repr 3) ? (
29do p1 ← clight_to_cminor myprog;
30do p2 ← cminor_to_rtlabs p1;
31 exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
32normalize
33%
34qed.
35
36(* The whole front end. *)
37
38example fe : finishes_with (repr 3) state (
39bind ? (snapshot state) (front_end myprog) (λp.
40exec_up_to RTLabs_fullexec p 1000 [ ])).
41normalize
42%
43qed.
44
Note: See TracBrowser for help on using the repository browser.