Commit baaee9e0 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix bugs in pointer operations

* Equality comparison of NULL and non NULL pointers should be defined
* Pointer comparisons, casts, and truth should only be defined for pointers
  that are alive
* Treat dead pointers as indeterminate values in refinements. The proofs that
  all operations preserve refinement indicate that dead pointers can be indeed
  by replaced by anything without affecting the program's behavior.
parent ab9e7cc8
......@@ -1260,12 +1260,12 @@ Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
| _, [] => right (prefix_of_nil_not _ _)
| x :: l1, y :: l2 =>
match decide_rel (=) x y with
| left Exy =>
| left Hxy =>
match go l1 l2 with
| left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Exy Hl1l2)
| left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Hxy Hl1l2)
| right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
end
| right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _)
| right Hxy => right (Hxy ∘ prefix_of_cons_inv_1 _ _ _ _)
end
end.
......
......@@ -500,11 +500,6 @@ Qed.
Lemma Z_to_option_of_nat x : Z_to_option_nat (Z.of_nat x) = Some x.
Proof. apply Z_to_option_nat_Some_alt. auto using Nat2Z.is_nonneg. Qed.
(** The function [Z_of_sumbool] converts a sumbool [P] into an integer
by yielding one if [P] and zero if [Q]. *)
Definition Z_of_sumbool {P Q : Prop} (p : {P} + {Q} ) : Z :=
(if p then 1 else 0)%Z.
(** Some correspondence lemmas between [nat] and [N] that are not part of the
standard library. We declare a hint database [natify] to rewrite a goal
involving [N] into a corresponding variant involving [nat]. *)
......
......@@ -209,14 +209,16 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
match x with Some _ => idtac | None => idtac | _ => fail 1 end;
let y := fresh in destruct o as [y|] eqn:?;
[change (x = f y) in H|change (x = None) in H]
| H : fmap (M:=option) _ ?o = ?x |- _ =>
| H : fmap (M:=option) ?f ?o = ?x |- _ =>
match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
match x with Some _ => idtac | None => idtac | _ => fail 1 end;
destruct o eqn:?
| H : ?x = fmap (M:=option) _ ?o |- _ =>
let y := fresh in destruct o as [y|] eqn:?;
[change (Some (f y) = x) in H|change (None = x) in H]
| H : ?x = fmap (M:=option) ?f ?o |- _ =>
match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
match x with Some _ => idtac | None => idtac | _ => fail 1 end;
destruct o eqn:?
let y := fresh in destruct o as [y|] eqn:?;
[change (x = Some (f y)) in H|change (x = None) in H]
| _ => progress case_decide
| _ => progress case_option_guard
end.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment