|
Last change
on this file since 2844 was
2737,
checked in by garnier, 8 years ago
|
|
Commit of current proof state for Clight to Cminor translation.
|
|
File size:
1.0 KB
|
| Line | |
|---|
| 1 | include "Cminor/Cminor_semantics.ma". |
|---|
| 2 | |
|---|
| 3 | (* Avoid aliasing in interstage proofs *) |
|---|
| 4 | |
|---|
| 5 | definition 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 | |
|---|
| 11 | definition 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 *) |
|---|
| 20 | include "common/StructuredTraces.ma". |
|---|
| 21 | |
|---|
| 22 | definition 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 | |
|---|
| 30 | definition cm_genv ≝ genv. |
|---|
| 31 | |
|---|
| 32 | definition cm_env ≝ env. |
|---|
| 33 | |
|---|
| 34 | definition cm_cont ≝ cont. |
|---|
| 35 | |
|---|
| 36 | definition cm_eval_expr ≝ eval_expr. |
|---|
| 37 | |
|---|
| 38 | definition CmState ≝ State. |
|---|
| 39 | |
|---|
| 40 | definition CmReturnstate ≝ Returnstate. |
|---|
| 41 | |
|---|
| 42 | definition CmCallstate ≝ Callstate. |
|---|
| 43 | |
|---|
Note: See
TracBrowser
for help on using the repository browser.
