From 054ce39caf060408f6555bcd0b6d90b5bf4c00c5 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 8 May 2013 07:59:10 +0000
Subject: Missing case: initialization of a global variable of type _Bool.
 Added corresponding test case.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2242 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Initializers.v      | 2 +-
 cfrontend/Initializersproof.v | 1 +
 test/regression/Makefile      | 2 +-
 test/regression/Results/bool  | 1 +
 test/regression/bool.c        | 2 ++
 5 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 657f6073..cb2f132c 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -147,7 +147,7 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   do v1 <- constval a;
   do v2 <- do_cast v1 (typeof a) ty;
   match v2, ty with
-  | Vint n, Tint I8 sg _ => OK(Init_int8 n)
+  | Vint n, Tint (I8|IBool) sg _ => OK(Init_int8 n)
   | Vint n, Tint I16 sg _ => OK(Init_int16 n)
   | Vint n, Tint I32 sg _ => OK(Init_int32 n)
   | Vint n, Tpointer _ _ => OK(Init_int32 n)
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index c2ca135c..2f29514b 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -504,6 +504,7 @@ Proof.
   destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto.
   destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
   simpl in H2; inv H2. assumption.
+  simpl in H2; inv H2. assumption. 
   inv EQ2. simpl in H2; inv H2. assumption.
   (* long *)
   destruct ty; inv EQ2. simpl in H2; inv H2. assumption.
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 0d5e4c43..b0663b14 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -11,7 +11,7 @@ LIBS=$(LIBMATH)
 TESTS=int32 int64 floats floats-basics \
   expr1 expr6 funptr2 initializers volatile1 volatile2 volatile3 \
   funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \
-  sizeof1 sizeof2 binops
+  sizeof1 sizeof2 binops bool
 
 # Can run, but only in compiled mode, and have reference output in Results
 
diff --git a/test/regression/Results/bool b/test/regression/Results/bool
index 923c6e2b..a8283b88 100644
--- a/test/regression/Results/bool
+++ b/test/regression/Results/bool
@@ -7,3 +7,4 @@ f = 0
 g = 1
 h = 1
 i = 0
+y = 1
diff --git a/test/regression/bool.c b/test/regression/bool.c
index 4f8ed809..e8d8b6e7 100644
--- a/test/regression/bool.c
+++ b/test/regression/bool.c
@@ -3,6 +3,7 @@
 #include <stdio.h>
 
 int x = 42;
+_Bool y = 777;
 
 int main()
 {
@@ -25,5 +26,6 @@ int main()
   printf("g = %d\n", g);
   printf("h = %d\n", h);
   printf("i = %d\n", i);
+  printf("y = %d\n", y);
   return 0;
 }
-- 
cgit