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

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

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

File size: 2.0 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' ≝ \fst (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 (\snd (clight_label myprog)) p1 in
40  exec_up_to RTLabs_fullexec p2 1000 [ ])).
41normalize
42%
43qed.
44
45include "RTLabs/CostCheck.ma".
46
47axiom MISSING:String.
48axiom EXTERNAL:String.
49
50definition readable_body ≝
51λfn. insert_sort ?
52       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
53       (elements ?? (f_graph fn)).
54(*
55example c2: result ? (
56  ! p1 ← clight_to_cminor (simplify_program (clight_label myprog));
57  let p2 ≝ cminor_to_rtlabs p1 in
58  match prog_funct … p2 with
59  [ nil ⇒ Error ? (msg MISSING)
60  | cons h _ ⇒
61    match \snd h with
62    [ External _ ⇒ Error ? (msg EXTERNAL)
63    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
64    ]
65  ]).
66normalize
67*)
68example c2: (
69  let 〈p0,init〉 ≝ clight_label myprog in
70  ! p1 ← clight_to_cminor (simplify_program p0);
71  let p2 ≝ cminor_to_rtlabs init p1 in
72  return (check_cost_program p2)) = OK … true.
73normalize
74%
75qed.
Note: See TracBrowser for help on using the repository browser.