Merge of the "volatile" branch:

- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 25 insertions, 0 deletions

diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index f14b6a9..e6fd809 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -138,6 +138,31 @@ Proof.
   unfold notint; red; intros. TrivialExists. 
 Qed.
 
+Theorem eval_boolval: unary_constructor_sound boolval Val.boolval.
+Proof.
+  assert (DFL: 
+    forall le a x,
+    eval_expr ge sp e m le a x ->
+     exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Cne Int.zero)) (a ::: Enil)) v
+           /\ Val.lessdef (Val.boolval x) v).
+  intros. TrivialExists. simpl. destruct x; simpl; auto.
+
+  red. induction a; simpl; intros; eauto. destruct o; eauto.
+(* intconst *)
+  destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
+(* cmp *)
+  inv H. simpl in H5.
+  destruct (eval_condition c vl m) as []_eqn. 
+  TrivialExists. simpl. inv H5. rewrite Heqo. destruct b; auto.
+  simpl in H5. inv H5. 
+  exists Vundef; split; auto. EvalOp; simpl. rewrite Heqo; auto.
+
+(* condition *)
+  inv H. destruct v1.
+  exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
+  exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
+Qed.
+
 Theorem eval_notbool: unary_constructor_sound notbool Val.notbool.
 Proof.
   assert (DFL: