source: src/Cminor/Cminor_abstract.ma @ 2677

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

Retain the pointer for the function called in front-end call states
so that we can do sensible stack costs.

File size: 955 bytes
Line 
1include "Cminor/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.