From 4a5f1db8abe7831649f6f15178958e0c57955a25 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 4 Sep 2019 11:49:32 +0200 Subject: Duplicate: exec_function_internal --- backend/Duplicate.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'backend/Duplicate.v') diff --git a/backend/Duplicate.v b/backend/Duplicate.v index ac67cfe1..8a78ee80 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -33,6 +33,15 @@ Proof. repeat (split; try reflexivity). Qed. +Remark transf_function_fnsig: forall f tf, transf_function f = OK tf -> fn_sig f = fn_sig tf. + Proof. apply transf_function_preserves. Qed. +Remark transf_function_fnparams: forall f tf, transf_function f = OK tf -> fn_params f = fn_params tf. + Proof. apply transf_function_preserves. Qed. +Remark transf_function_fnstacksize: forall f tf, transf_function f = OK tf -> fn_stacksize f = fn_stacksize tf. + Proof. apply transf_function_preserves. Qed. +Remark transf_function_fnentrypoint: forall f tf, transf_function f = OK tf -> fn_entrypoint f = fn_entrypoint tf. + Proof. apply transf_function_preserves. Qed. + Definition transf_fundef (f: fundef) : res fundef := transf_partial_fundef transf_function f. -- cgit