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

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

A pointer comparison test case that illustrates a bug.

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