diff options
Diffstat (limited to 'cfrontend/Initializersproof.v')
| -rw-r--r-- | cfrontend/Initializersproof.v | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index ca9c5b0..b64c309 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -380,6 +380,13 @@ Proof. eelim Mem.perm_empty; eauto. Qed. +Lemma mem_empty_not_weak_valid_pointer: + forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false. +Proof. + intros. unfold Mem.weak_valid_pointer. + now rewrite !mem_empty_not_valid_pointer. +Qed. + Lemma sem_cmp_match: forall c v1 ty1 v2 ty2 m v v1' v2' v', sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v -> @@ -391,10 +398,12 @@ Opaque zeq. intros. unfold sem_cmp in *. destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval. destruct (Int.eq n Int.zero); try discriminate. - unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor. + unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor. destruct (Int.eq n Int.zero); try discriminate. - unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor. - rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. discriminate. + unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor. + rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. + rewrite (mem_empty_not_weak_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. simpl in H4. + destruct (zeq (Z.pos id) (Z.pos id0)); discriminate. Qed. Lemma sem_binary_match: |