From 98004b386dcc3e57e6a939a33fb7db903910d02d Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 3 Sep 2019 18:24:18 +0200 Subject: Duplicate: match_states --- backend/Duplicateproof.v | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'backend/Duplicateproof.v') 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). -- cgit