Let the malloc expression non-deterministically yield NULL.

* This behavior is "implementation defined" and can be turned on and off
  using the Boolean field "alloc_can_fail" of the class "Env".
* The expression "EAlloc" is now an r-value of pointer type instead of an
  l-value.
* The executable semantics for expressions is now non-deterministic. Hence,
  some proofs had to be revised.

theories/base.v

@@ -734,6 +734,7 @@ Class FreshSpec A C `{ElemOf A C,
 (** The following coercion allows us to use Booleans as propositions. *)
 Coercion Is_true : bool >-> Sortclass.
 Hint Unfold Is_true.
+Hint Immediate Is_true_eq_left.
 Hint Resolve orb_prop_intro andb_prop_intro.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).

theories/collections.v

@@ -95,6 +95,7 @@ End simple_collection.
 
 Definition of_option `{Singleton A C} `{Empty C} (x : option A) : C :=
   match x with None => ∅ | Some a => {[ a ]} end.
+
 Lemma elem_of_of_option `{SimpleCollection A C} (x : A) o :
   x ∈ of_option o ↔ o = Some x.
 Proof.
@@ -103,12 +104,27 @@ Qed.
 
 Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
   λ P dec A x, match dec with left H => x H | _ => ∅ end.
-Lemma elem_of_guard `{CollectionMonad M} `{Decision P} {A} (x : A) (X : M A) :
-  x ∈ guard P; X ↔ P ∧ x ∈ X.
-Proof.
-  unfold mguard, collection_guard; simpl; case_match;
-    rewrite ?elem_of_empty; naive_solver.
-Qed.
+
+Section collection_monad_base.
+  Context `{CollectionMonad M}.
+  Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
+    x ∈ guard P; X ↔ P ∧ x ∈ X.
+  Proof.
+    unfold mguard, collection_guard; simpl; case_match;
+      rewrite ?elem_of_empty; naive_solver.
+  Qed.
+  Lemma guard_empty `{Decision P} {A} (X : M A) : guard P; X ≡ ∅ ↔ ¬P ∨ X ≡ ∅.
+  Proof.
+    rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
+    destruct (decide P); naive_solver.
+  Qed.
+  Lemma bind_empty {A B} (f : A → M B) X :
+    X ≫= f ≡ ∅ ↔ X ≡ ∅ ∨ ∀ x, x ∈ X → f x ≡ ∅.
+  Proof.
+    setoid_rewrite elem_of_equiv_empty; setoid_rewrite elem_of_bind.
+    naive_solver.
+  Qed.
+End collection_monad_base.
 
 (** * Tactics *)
 (** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will
@@ -160,6 +176,7 @@ Ltac decompose_empty := repeat
   | H : _ ∪ _ = ∅ |- _ => apply empty_union_L in H; destruct H
   | H : _ ∪ _ ≠ ∅ |- _ => apply non_empty_union_L in H; destruct H
   | H : {[ _ ]} = ∅ |- _ => destruct (non_empty_singleton_L _ H)
+  | H : guard _ ; _ ≡ ∅ |- _ => apply guard_empty in H; destruct H
   end.
 
 (** The first pass of our collection tactic consists of eliminating all
@@ -462,6 +479,10 @@ Section collection_monad.
     Proper ((≡) ==> (≡)) (@mjoin M _ A).
   Proof. intros X Y E. esolve_elem_of. Qed.
 
+  Lemma collection_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
+  Proof. esolve_elem_of. Qed.
+  Lemma collection_guard_True {A} `{Decision P} (X : M A) : P → guard P; X ≡ X.
+  Proof. esolve_elem_of. Qed.
   Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) X :
     g ∘ f <$> X ≡ g <$> (f <$> X).
   Proof. esolve_elem_of. Qed.

theories/option.v

@@ -239,6 +239,8 @@ Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
     let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
   | H : context [default (A:=?A) _ ?o _] |- _ =>
     let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
+  | H : context [from_option (A:=?A) _ ?o] |- _ =>
+    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
   | H : context [ match ?o with _ => _ end ] |- _ =>
     match type of o with
     | option ?A =>