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

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

Update some test cases.

File size: 1.1 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/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/RTLabs_semantics.ma".
22
23example e2: finishes_with (repr 3) ? (
24let 〈p0,init〉 ≝ clight_label myprog in
25bind ? (snapshot state) (clight_to_cminor p0) (λp1.
26let p2 ≝ cminor_to_rtlabs init p1 in
27 exec_up_to RTLabs_fullexec p2 1000 [ ])).
28(*
29example e2: finishes_with (repr 3) ? (
30do p1 ← clight_to_cminor myprog;
31do p2 ← cminor_to_rtlabs p1;
32 exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
33normalize
34%
35qed.
36
37(* The whole front end. *)
38
39example fe : finishes_with (repr 3) state (
40bind ? (snapshot state) (front_end myprog) (λp.
41exec_up_to RTLabs_fullexec (\snd p) 1000 [ ])).
42normalize
43%
44qed.
45
Note: See TracBrowser for help on using the repository browser.