diff options
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 74a6da5..ad5ada6 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -574,7 +574,8 @@ Proof. inversion H8. eauto with cshm. (* pp ptr ptr *) inversion H10. eapply eval_Ebinop; eauto with cshm. - simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. auto. + simpl. unfold Val.cmpu. simpl. unfold Mem.weak_valid_pointer in *. + rewrite H3. rewrite H9. auto. inversion H10. eapply eval_Ebinop; eauto with cshm. simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. destruct cmp; simpl in *; inv H; auto. |