source: src/Clight/test/endptr2.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.7 KB
Line 
1include "Clight/test/endptr2.c.ma".
2
3example exec: exec_up_to clight_fullexec myprog 1000 [ ] = Error ? (msg FailedOp).
4normalize  (* you can examine the result here *)
5%
6qed.
7
8include "Clight/SimplifyCasts.ma".
9include "Clight/toCminor.ma".
10include "Cminor/Cminor_semantics.ma".
11
12example e1:
13  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
14   (λp. exec_up_to Cminor_fullexec p 1000 [ ]))
15  = Error ? (msg FailedOp).
16normalize
17%
18qed.
19
20include "Cminor/toRTLabs.ma".
21include "RTLabs/RTLabs_semantics.ma".
22include "Clight/label.ma".
23
24example e2:
25let 〈p0,init〉 ≝ clight_label myprog in
26bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
27(λp1. let p2 ≝ cminor_to_rtlabs init p1 in
28  exec_up_to RTLabs_fullexec p2 1000 [ ])
29= Error ? (msg FailedOp).
30normalize
31%
32qed.
33
34include "RTLabs/CostCheck.ma".
35
36definition readable_body ≝
37λfn. insert_sort ?
38       (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z]))
39       (elements ?? (f_graph fn)).
40(*
41example c2: result ? (
42  let 〈p0,init〉 ≝ clight_label myprog in
43  ! p1 ← clight_to_cminor (simplify_program p0);
44  let p2 ≝ cminor_to_rtlabs init p1 in
45  match prog_funct … p2 with
46  [ nil ⇒ Error ? (msg MISSING)
47  | cons h _ ⇒
48    match \snd h with
49    [ External _ ⇒ Error ? (msg EXTERNAL)
50    | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉
51    ]
52  ]).
53normalize
54*)
55example c2: (
56  let 〈p0,init〉 ≝ clight_label myprog in
57  ! p1 ← clight_to_cminor (simplify_program p0);
58  let p2 ≝ cminor_to_rtlabs init p1 in
59  return (check_cost_program p2)) = OK bool true.
60normalize
61%
62qed.
63
64
65
66(*
67include "RTLabs/RTLabsToRTL.ma".
68include alias "basics/lists/list.ma".
69
70definition take_out: ∀A. res A → A ≝
71 λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?].
72cases daemon
73qed.
74
75example CSC: True.
76letin xxx ≝
77 (let p ≝ take_out … (clight_to_cminor myprog) in
78  let p ≝ take_out … (cminor_to_rtlabs p) in
79(*   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *)
80  let p ≝ rtlabs_to_rtl p in
81   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p))
82 )
83[2: cases daemon]
84normalize in xxx;
85
86
87[2:
88  OK (list (codeT (prog_var_names … p) (rtl_params (prog_var_names … p)))) (list_map … (λx. match (\snd x) return λ_.codeT (prog_var_names … p) (rtl_params ?) with [External _ ⇒ ? | Internal f ⇒ ?(*joint_if_code ? (rtl_params ?) f*)]) (prog_funct … p)))
89(*  OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)))
90*)
91[2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon  ]
92normalize in xxx
93*)
Note: See TracBrowser for help on using the repository browser.