source: src/Clight/test/implicitcond.test.ma @ 2568

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

Relax some Clight type checks to Cminor type checks to avoid array/pointer
confusion. Drop a dead function.

File size: 1.8 KB
Line 
1include "Clight/test/implicitcond.c.ma".
2
3example exec: finishes_with (repr I32 2) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
4normalize  (* you can examine the result here *)
5%
6qed.
7
8include "Clight/SimplifyCasts.ma".
9
10example es: finishes_with (repr I32 2) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
11normalize  (* you can examine the result here *)
12%
13qed.
14
15include "Clight/toCminor.ma".
16include "Cminor/semantics.ma".
17
18example e1: finishes_with (repr I32 2) ?
19  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
20   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
21normalize
22%
23qed.
24
25include "Cminor/toRTLabs.ma".
26include "RTLabs/semantics.ma".
27include "Clight/label.ma".
28
29example e2: finishes_with (repr I32 2) ? (
30let 〈p0,init〉 ≝ clight_label myprog in
31bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
32(λp1. let p2 ≝ cminor_to_rtlabs init p1 in
33  exec_up_to RTLabs_fullexec p2 1000 [ ])).
34normalize
35%
36qed.
37
38include "RTLabs/CostCheck.ma".
39
40axiom MISSING:String.
41axiom EXTERNAL:String.
42
43definition readable_body ≝
44λfn. insert_sort ?
45       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
46       (elements ?? (f_graph fn)).
47(*
48example c2: result ? (
49  let 〈p0,init〉 ≝ clight_label myprog in
50  ! p1 ← clight_to_cminor (simplify_program p0);
51  let p2 ≝ cminor_to_rtlabs init p1 in
52  match prog_funct … p2 with
53  [ nil ⇒ Error ? (msg MISSING)
54  | cons h _ ⇒
55    match \snd h with
56    [ External _ ⇒ Error ? (msg EXTERNAL)
57    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
58    ]
59  ]).
60normalize
61*)
62example c2: (
63  let 〈p0,init〉 ≝ clight_label myprog in
64  ! p1 ← clight_to_cminor (simplify_program p0);
65  let p2 ≝ cminor_to_rtlabs init p1 in
66  return (check_cost_program p2)) = OK bool true.
67normalize
68%
69qed.
70
71
Note: See TracBrowser for help on using the repository browser.