Merge of branch seq-and-or. See Changelog for details.

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

1 files changed, 16 insertions, 0 deletions

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index b4e3984..41dbe3f 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -82,6 +82,22 @@ Fixpoint constval (a: expr) : res val :=
       OK (Vint (Int.repr (sizeof ty1)))
   | Ealignof ty1 ty =>
       OK (Vint (Int.repr (alignof ty1)))
+  | Eseqand r1 r2 ty =>
+      do v1 <- constval r1;
+      do v2 <- constval r2;
+      match bool_val v1 (typeof r1) with
+      | Some true => do v3 <- do_cast v2 (typeof r2) type_bool; do_cast v3 type_bool ty
+      | Some false => OK (Vint Int.zero)
+      | None => Error(msg "undefined && operation")
+      end
+  | Eseqor r1 r2 ty =>
+      do v1 <- constval r1;
+      do v2 <- constval r2;
+      match bool_val v1 (typeof r1) with
+      | Some false => do v3 <- do_cast v2 (typeof r2) type_bool; do_cast v3 type_bool ty
+      | Some true => OK (Vint Int.one)
+      | None => Error(msg "undefined || operation")
+      end
   | Econdition r1 r2 r3 ty =>
       do v1 <- constval r1;
       do v2 <- constval r2;