diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-04 11:49:32 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-04 11:49:32 +0200 |
| commit | 4a5f1db8abe7831649f6f15178958e0c57955a25 (patch) | |
| tree | 9c7c227494b39b5b6d2228983ee228309caba1f2 /backend/Duplicate.v | |
| parent | f91f8296b6d2f663878223d473cd9e887403f73f (diff) | |
| download | compcert-kvx-4a5f1db8abe7831649f6f15178958e0c57955a25.tar.gz compcert-kvx-4a5f1db8abe7831649f6f15178958e0c57955a25.zip | |
Duplicate: exec_function_internal
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |