From 2db8b0c27199667326f82c655a9e26c44ddce748 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 3 Mar 2020 11:22:44 +0100
Subject: [PATCH] [typing] don't forget to cast result of conditional if needed
---
src/kernel_internals/typing/cabs2cil.ml | 2 ++
tests/syntax/compile_constant.c | 6 +++++-
tests/syntax/oracle/compile_constant.res.oracle | 2 +-
3 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index a8bbbf71239..fae93b76c43 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7233,9 +7233,11 @@ and doExp local_env
clean_up_chunk_locals se2;
let loc = e2.expr_loc in
let e2' = match e2'o with None -> Cil.one ~loc | Some e -> e in
+ let _,e2' = castTo t2 tresult e2' in
finishExp [] empty e2' tresult;
end else if asconst <> CNoConst && is_true_cond = `CFalse then begin
clean_up_chunk_locals se3;
+ let _,e3' = castTo t3 tresult e3' in
finishExp [] empty e3' tresult
end else begin
if not (isEmpty se2) then
diff --git a/tests/syntax/compile_constant.c b/tests/syntax/compile_constant.c
index 7950752d64c..c72ac927b6e 100644
--- a/tests/syntax/compile_constant.c
+++ b/tests/syntax/compile_constant.c
@@ -1,12 +1,16 @@
#define M0(x) (x)*(x)<4.0?0.0:1.0
char pixels[] = {M0(0.0), M0(1), M0(2.0f)};
+/* tests below should evaluate to 2. */
+
char test_neg = { (-0.) ? 1. : 2. };
char test_ge = { ((-1.) >= 0.) ? 1. : 2. };
-char test_cast = { 1 >= (0?1U:(-1)) ? 1. : 2. };
+char test_cast[] = { 1 >= (0?1U:(-1)) ? 1. : 2.,
+ ((double)1) >= (0?1U:(-1)) ? 1. : 2. };
extern int f(void);
+/* no call should be evaluated. */
char no_call[] = { 1 ? 1 : f(), 0?f():2 };
diff --git a/tests/syntax/oracle/compile_constant.res.oracle b/tests/syntax/oracle/compile_constant.res.oracle
index dd041c0148f..b9baaf82b3c 100644
--- a/tests/syntax/oracle/compile_constant.res.oracle
+++ b/tests/syntax/oracle/compile_constant.res.oracle
@@ -3,6 +3,6 @@
char pixels[3] = {(char)0.0, (char)0.0, (char)1.0};
char test_neg = (char)2.;
char test_ge = (char)2.;
-char test_cast = (char)2.;
+char test_cast[2] = {(char)2., (char)2.};
char no_call[2] = {(char)1, (char)2};
--
GitLab