diff options
| -rw-r--r-- | cfrontend/Initializers.v | 2 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 1 | ||||
| -rw-r--r-- | test/regression/Makefile | 2 | ||||
| -rw-r--r-- | test/regression/Results/bool | 1 | ||||
| -rw-r--r-- | test/regression/bool.c | 2 |
5 files changed, 6 insertions, 2 deletions
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 657f607..cb2f132 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 c2ca135..2f29514 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 0d5e4c4..b0663b1 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 923c6e2..a8283b8 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 4f8ed80..e8d8b6e 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; } |