diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 16:30:44 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 16:30:44 +0100 |
| commit | 04a46f516487557df00f43453c8decbc8567c458 (patch) | |
| tree | 4ec5bcbbef0ff74ef3923b0f8d1bec8fedf3be75 /backend/Duplicateproof.v | |
| parent | 361977d47b586dc2f8dec71f597e7f802de8dffa (diff) | |
| download | compcert-kvx-04a46f516487557df00f43453c8decbc8567c458.tar.gz compcert-kvx-04a46f516487557df00f43453c8decbc8567c458.zip | |
Modified the hook for the oracle
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index ebb17774..67d16580 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -76,7 +76,8 @@ Theorem transf_function_preserves: transf_function f = OK f' -> fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'. Proof. - intros. unfold transf_function in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. + intros. unfold transf_function in H. destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te). + monadInv H. repeat (split; try reflexivity). Qed. @@ -227,7 +228,7 @@ Theorem transf_function_correct f f': Proof. unfold transf_function. intros TRANSF. - destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). + destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te). monadInv TRANSF. unfold verify_mapping in EQ. monadInv EQ. exists mp; constructor 1; simpl; auto. |