Source: http://compcert.inria.fr/verasco/coqdoc/1.3/html/NoError.html
Timestamp: 2019-04-18 15:02:36+00:00

Document:
Context (ge: genv) (e: env) (t: temp_env) (m: Mem.mem).
t ! id = Some v.
eval_constant c = Some v.
∃ b, eval_var_addr ge e id b ∧ v = Vptr b Int.zero.
eval_unop op v' = Some v.
eval_binop op v1 v2 m = Some v.
∃ v', eval_expr ge e t m a v' ∧ Mem.loadv κ m v' = Some v.
Let valid_ptr : block → Z → bool := Mem.valid_pointer m.
Let weak_valid_ptr := λ b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1).
∨ (∃ v, eval_expr ge e t m q v ∧ error_expr r).
Val.cmp c (Vint i) (Vint j) = Vundef → False.
unfold Val.cmp. simpl. destruct Int.cmp; discriminate. Qed.
Val.cmpf c (Vfloat f) (Vfloat g) = Vundef → False.
unfold Val.cmpf. simpl. destruct Float.cmp; discriminate. Qed.
Val.cmpfs c (Vsingle f) (Vsingle g) = Vundef → False.
unfold Val.cmpfs. simpl. destruct Float32.cmp; discriminate. Qed.
Val.of_bool b = Vundef → False.
Hint Resolve val_cmp_ii_def val_cmpf_ff_def val_cmpfs_ss_def val_of_bool_def.
∀ v, eval_expr ge e t m q v → v ≠ Vundef.
eval_expr_inv; try (elim NB; vauto; discriminate).
+ destruct c; simpl in *; eq_some_inv; discriminate.
+ assert (¬ error_expr q) as NB'.
end;[simpl in *; eq_some_inv; discriminate|elim NB; vauto; fail]).
[discriminate| elim NB; vauto; fail]).
destruct (eq_block b b0) as [ ? | NE ]. discriminate.
destruct (Int.eq i0 Int.zero); simpl in *. eq_some_inv.
destruct (Int.eq i (Int.repr Int.min_signed)).
simpl in *; eq_some_inv; discriminate.
destruct (Int.eq i0 Int.zero); simpl in *; eq_some_inv.
destruct (Int64.eq i0 Int64.zero); simpl in *. eq_some_inv.
destruct (Int64.eq i (Int64.repr Int64.min_signed)).
destruct (Int64.eq i0 Int64.zero); simpl in *; eq_some_inv.
unfold Val.cmpu in *. simpl in *. destruct Int.cmpu; discriminate.
unfold Val.cmpu in *. simpl in *.
|| Mem.valid_pointer m b (Int.unsigned i0 - 1))) eqn: Z.
elim NB. rewrite Bool.andb_false_iff in Z. destruct Z; vauto.
|| Mem.valid_pointer m b (Int.unsigned i - 1))) eqn: Z.
assert (∀ b : bool, (if b then Vtrue else Vfalse) ≠ Vundef) as K.
destruct (eq_block b b0). subst b0.
apply NB. eapply error_Ebinop; eauto.
apply error_Ocmpu_pp_winvalid; unfold weak_valid_ptr, valid_ptr.
right; rewrite Hi0, Hi0'; reflexivity.
left; rewrite Hi, Hi'; reflexivity.
destruct c; try discriminate; apply NB; vauto; fail.
destruct c; simpl in *; eq_some_inv; eauto.
assert (¬ error_expr q) as NB'.
destruct v1; try (elim NB; vauto; fail).
∃ v, eval_expr ge e t m q v.
+ destruct (t ! i) as [v|] eqn:?. vauto.
+ destruct (e ! i) as [(b,o)|] eqn:?. vauto2.
destruct (Genv.find_symbol ge i) as [b|] eqn: ?. vauto2.
specialize (IHq NB'); clear NB'.
destruct IHq as (v & EV).
try (eexists; econstructor; eauto; simpl; try rewrite EQ; reflexivity).
specialize (IHq1 NB1); clear NB1.
destruct IHq1 as (v1 & V1).
specialize (IHq2 NB2); clear NB2.
destruct IHq2 as (v2 & V2).
destruct v2; try (elim NB; vauto; fail).
destruct (Int.eq i0 Int.zero) eqn: Z.
intros ->. elim NB. vauto.
generalize (Int.eq_spec i (Int.repr Int.min_signed)).
destruct (Int.eq i (Int.repr Int.min_signed)) eqn: MS.
destruct (Int.eq i0 Int.mone) eqn: M1.
simpl; rewrite Z, MS, M1; reflexivity.
simpl; rewrite Z, MS; reflexivity.
destruct (Int64.eq i0 Int64.zero) eqn: Z.
generalize (Int64.eq_spec i (Int64.repr Int64.min_signed)).
destruct (Int64.eq i (Int64.repr Int64.min_signed)) eqn: MS.
destruct (Int64.eq i0 Int64.mone) eqn: M1.
destruct v; try (elim NB; vauto; fail).
destruct (Mem.load m0 m b (Int.unsigned i)) as [v|] eqn:?.
∃ v, v ≠ Vundef ∧ eval_expr ge e t m q v.
destruct (noerror_eval_expr NB) as (v & EV).
exists v. eauto using noerror_def.
Context (var: Type) (ρ: var → val) (ε: ident → option block).
Let eval_pexpr := eval_pexpr ge m ρ ε.
∀ v, eval_pexpr pe v → v ≠ Vundef.
eval_pexpr_inv; subst; intros K; subst; hsplit; try discriminate.
- simpl in *. apply NB.
- assert ( ¬ error_pexpr pe ) as NB' by (intros ?; elim NB; vauto).
specialize (IHpe NB'); clear NB'.
subst. fold (eval_pexpr pe) in *.
end;[simpl in *; eq_some_inv; discriminate|apply NB; right; eexists; split; [ exact EV | vauto2 ]]).
[discriminate| apply NB; right; eexists; split; [ exact EV | right; eexists; vauto2 ]]).
apply NB; right; eexists; split; [ eauto | right; eexists; split; [ eauto | vauto ] ].
elim NB; right; eexists; split; eauto; right; eexists; split; eauto; vauto.
elim NB; right; eexists; split; eauto; right; eexists; split; eauto.
rewrite Bool.andb_false_iff in Z. destruct Z; vauto.
apply NB. right. eexists; split; eauto. right. eexists; split; eauto.
destruct (Int.cmpu _ _ _); discriminate. intros _.
rewrite andb_false_iff in *. assumption.
destruct c; try discriminate; vauto.

References: v.

 v.

 v.

 v.

 v.

 v.

 v.

 v.