diff options
Diffstat (limited to 'x86/ConstpropOpproof.v')
| -rw-r--r-- | x86/ConstpropOpproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v index 5eb46e34..ce20738c 100644 --- a/x86/ConstpropOpproof.v +++ b/x86/ConstpropOpproof.v @@ -292,8 +292,10 @@ Lemma addr_strength_reduction_correct: exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'. Proof. unfold eval_addressing, addr_strength_reduction. destruct Archi.ptr64. +- intros until res. destruct (addressing_valid (fst (addr_strength_reduction_64 addr args vl))). apply addr_strength_reduction_64_correct. - apply addr_strength_reduction_32_correct. + intros; exists res; auto. +- apply addr_strength_reduction_32_correct. Qed. Lemma make_cmp_base_correct: |