source: src/Cminor/abstract.ma @ 2598

Last change on this file since 2598 was 2598, checked in by garnier, 8 years ago

Tentative, partial draft for the definition of Clight-Cminor simulation for statements. Commented out for now.
Also, some stuff on memory injections, and some more aliases on abstract.ma.

File size: 946 bytes
Line 
1include "Cminor/semantics.ma".
2
3(* Avoid aliasing in interstage proofs *)
4
5definition Cminor_state ≝ state.
6
7(* States about to execute a cost statement.  Other statements may also emit
8   cost labels due to expressions, but these are the only ones relevant for
9   defining measurable subtraces. *)
10
11definition Cminor_labelled : state → bool ≝
12λs. match s with
13[ State _ st _ _ _ _ _ _ _ _ ⇒ match st with [ St_cost _ _ ⇒ true | _ ⇒ false ]
14| _ ⇒ false
15].
16
17(* Usual classification *)
18
19(* only for classification type *)
20include "common/StructuredTraces.ma".
21
22definition Cminor_classify : state → status_class ≝
23λs. match s with
24[ State _ _ _ _ _ _ _ _ _ _ ⇒ cl_other
25| Callstate _ _ _ _ ⇒ cl_call
26| Returnstate _ _ _ ⇒ cl_return
27| Finalstate _ ⇒ cl_other
28].
29
30definition cm_genv ≝ genv.
31
32definition cm_env ≝ env.
33
34definition cm_cont ≝ cont.
35
36definition cm_eval_expr ≝ eval_expr.
37
38definition CmState ≝ State.
39
Note: See TracBrowser for help on using the repository browser.