source: src/Clight/test/endptr.test.ma @ 2395

Last change on this file since 2395 was 2395, checked in by campbell, 8 years ago

Proper handling of comparison of pointers off-the-end of an object.
We might need to drop this if the proofs/back-end work is too involved.

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