From 63f779c5951eb957cb5b36d24e0daf58dac69d55 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 30 Aug 2022 17:50:46 +0200
Subject: [PATCH] [typing] better handling of casts to boolean
- Cabs2cil.is_boolean_result returns true if the expression is of type _Bool
- use standard result instead of custom expression for cast of a boolean to _Bool
---
src/kernel_internals/typing/cabs2cil.ml | 3 ++-
tests/syntax/oracle/bool_conversion.res.oracle | 4 ++--
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4bfb3e211bb..aeda98b6756 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1403,6 +1403,7 @@ let dropQualifiers = Cil.type_remove_qualifier_attributes
(* true if the expression is known to be a boolean result, i.e. 0 or 1. *)
let rec is_boolean_result e =
+ Cil.(isBoolType (typeOf e)) ||
match e.enode with
| Const _ ->
(match Cil.isInteger e with
@@ -2932,7 +2933,7 @@ let rec castTo ?context ?(fromsource=false)
| t, TInt(IBool,_) when is_scalar_type t ->
if is_boolean_result e then begin
Kernel.debug ~dkey "Explicit cast to Boolean: %a" Cil_printer.pp_exp e;
- nt,Cil.mkCastT ~oldt:ot ~newt:nt e
+ result
end else begin
Kernel.debug ~dkey
"bool conversion by checking !=0: %a" Cil_printer.pp_exp e;
diff --git a/tests/syntax/oracle/bool_conversion.res.oracle b/tests/syntax/oracle/bool_conversion.res.oracle
index 1dc3bc0af15..11c18ae513c 100644
--- a/tests/syntax/oracle/bool_conversion.res.oracle
+++ b/tests/syntax/oracle/bool_conversion.res.oracle
@@ -12,10 +12,10 @@ void main(void)
_Bool tmp;
_Bool tmp_1;
tmp = get_bool();
- if ((_Bool)((int)tmp != 0)) tmp_0 = 0; else tmp_0 = 1;
+ if (tmp) tmp_0 = 0; else tmp_0 = 1;
b_flag1 = pass_bool((_Bool)(tmp_0 != 0));
tmp_1 = get_bool();
- b_flag2 = pass_bool((_Bool)((int)tmp_1 != 0));
+ b_flag2 = pass_bool(tmp_1);
return;
}
--
GitLab