diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-04-01 18:27:15 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-04-01 18:27:15 +0200 |
commit | 68e2ce02f8d69b26c9cea6e0d338f855cbea3ace (patch) | |
tree | 98acb09c398112bff31ce34c0857aa0f4e9b8e23 /cfrontend/Cshmgenproof.v | |
parent | 5d6febecb8c0f90a627033744f6f62164645a1a4 (diff) | |
parent | daccc2928e6410c4e8c886ea7d019fd9a071b931 (diff) | |
download | compcert-68e2ce02f8d69b26c9cea6e0d338f855cbea3ace.tar.gz compcert-68e2ce02f8d69b26c9cea6e0d338f855cbea3ace.zip |
Merge pull request #31 from AbsInt/null-ptr-cmp
Revised semantics of comparisons between a pointer and 0.
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
-rw-r--r-- | cfrontend/Cshmgenproof.v | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 7f61c657..025d7b66 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -311,7 +311,7 @@ Qed. Lemma make_boolean_correct: forall e le m a v ty b, eval_expr ge e le m a v -> - bool_val v ty = Some b -> + bool_val v ty m = Some b -> exists vb, eval_expr ge e le m (make_boolean a ty) vb /\ Val.bool_of_val vb b. @@ -333,7 +333,10 @@ Proof. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. - exists Vtrue; split. econstructor; eauto with cshm. constructor. + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2. + unfold Val.cmpu, Val.cmpu_bool. simpl. + unfold Mem.weak_valid_pointer in V; rewrite V. constructor. (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. @@ -366,13 +369,16 @@ Qed. Lemma make_notbool_correct: forall a tya c va v e le m, - sem_notbool va tya = Some v -> + sem_notbool va tya m = Some v -> make_notbool a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1; destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0. + econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Mem.weak_valid_pointer in V; rewrite V. auto. Qed. Lemma make_notint_correct: @@ -633,7 +639,7 @@ Qed. Lemma transl_unop_correct: forall op a tya c va v e le m, transl_unop op a tya = OK c -> - sem_unary_operation op va tya = Some v -> + sem_unary_operation op va tya m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. |