diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-03 18:24:18 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-03 18:24:18 +0200 |
| commit | 98004b386dcc3e57e6a939a33fb7db903910d02d (patch) | |
| tree | f82917ec1d595ddcba582881965441cb8af6f26f /backend/Duplicateproof.v | |
| parent | 853d2e0ef514281f6e6459212dc2142d5d3a90a0 (diff) | |
| download | compcert-kvx-98004b386dcc3e57e6a939a33fb7db903910d02d.tar.gz compcert-kvx-98004b386dcc3e57e6a939a33fb7db903910d02d.zip | |
Duplicate: match_states
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 65c07b45..264b7dff 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -84,10 +84,18 @@ Inductive match_states: state -> state -> Prop := | match_states_intro: forall st f sp pc rs m st' f' pc' (STACKS: list_forall2 match_stackframes st st') - (TRANSF: transf_function f = OK f') + (TRANSL: transf_function f = OK f') (DUPLIC: match_nodes f pc pc'), match_states (State st f sp pc rs m) (State st' f' sp pc' rs m) - (* TODO - fill the rest *). + | match_states_call: + forall st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: transf_fundef f = OK f'), + match_states (Callstate st f args m) (Callstate st' f' args m) + | match_states_return: + forall st st' v m + (STACKS: list_forall2 match_stackframes st st'), + match_states (Returnstate st v m) (Returnstate st' v m). Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). |