diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-11 16:51:47 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-11 16:51:47 +0200 |
| commit | 417b6e77e5a0c4ea3431d5f379ff054a26b1e326 (patch) | |
| tree | 9a2da7aedccf9d07aed0aa95e3167819c6047e25 /backend/Duplicate.v | |
| parent | 5361fd9e5bfb9a1c80103cf83a06427b24b57369 (diff) | |
| download | compcert-kvx-417b6e77e5a0c4ea3431d5f379ff054a26b1e326.tar.gz compcert-kvx-417b6e77e5a0c4ea3431d5f379ff054a26b1e326.zip | |
Fixing Linking problem
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 5c0b1d58..cb3936bb 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -34,35 +34,35 @@ Definition verify_mapping (xf: xfunction) (tc: code) (tentry: node) : res unit : (** * Entry points *) -Definition transf_function (f: function) : res xfunction := +Definition transf_function_aux (f: function) : res xfunction := let (tcte, mp) := duplicate_aux f in let (tc, te) := tcte in let xf := {| fn_RTL := (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te); fn_revmap := mp |} in do u <- verify_mapping xf tc te; OK xf. -Theorem transf_function_preserves: +Theorem transf_function_aux_preserves: forall f xf, - transf_function f = OK xf -> + transf_function_aux f = OK xf -> fn_sig f = fn_sig (fn_RTL xf) /\ fn_params f = fn_params (fn_RTL xf) /\ fn_stacksize f = fn_stacksize (fn_RTL xf). Proof. - intros. unfold transf_function in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. + intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. repeat (split; try reflexivity). Qed. -Remark transf_function_fnsig: forall f xf, transf_function f = OK xf -> fn_sig f = fn_sig (fn_RTL xf). - Proof. apply transf_function_preserves. Qed. -Remark transf_function_fnparams: forall f xf, transf_function f = OK xf -> fn_params f = fn_params (fn_RTL xf). - Proof. apply transf_function_preserves. Qed. -Remark transf_function_fnstacksize: forall f xf, transf_function f = OK xf -> fn_stacksize f = fn_stacksize (fn_RTL xf). - Proof. apply transf_function_preserves. Qed. +Remark transf_function_aux_fnsig: forall f xf, transf_function_aux f = OK xf -> fn_sig f = fn_sig (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. +Remark transf_function_aux_fnparams: forall f xf, transf_function_aux f = OK xf -> fn_params f = fn_params (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. +Remark transf_function_aux_fnstacksize: forall f xf, transf_function_aux f = OK xf -> fn_stacksize f = fn_stacksize (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. -Definition transf_fundef_aux (f: fundef) : res xfundef := - transf_partial_fundef transf_function f. +Definition transf_function (f: function) : res function := + do xf <- transf_function_aux f; + OK (fn_RTL xf). -Definition transf_fundef (f: fundef): res fundef := - do xf <- transf_fundef_aux f; - OK (fundef_RTL xf). +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. Definition transf_program (p: program) : res program := transform_partial_program transf_fundef p.
\ No newline at end of file |