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

Last change on this file was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
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/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/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
47definition readable_body ≝
48λfn. insert_sort ?
49       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
50       (elements ?? (f_graph fn)).
51(*
52example c2: result ? (
53  ! p1 ← clight_to_cminor (simplify_program (clight_label myprog));
54  let p2 ≝ cminor_to_rtlabs p1 in
55  match prog_funct … p2 with
56  [ nil ⇒ Error ? (msg MISSING)
57  | cons h _ ⇒
58    match \snd h with
59    [ External _ ⇒ Error ? (msg EXTERNAL)
60    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
61    ]
62  ]).
63normalize
64*)
65example c2: (
66  let 〈p0,init〉 ≝ clight_label myprog in
67  ! p1 ← clight_to_cminor (simplify_program p0);
68  let p2 ≝ cminor_to_rtlabs init p1 in
69  return (check_cost_program p2)) = OK … true.
70normalize
71%
72qed.
Note: See TracBrowser for help on using the repository browser.