From f008db55d57cbc07cc922ca477fbe0214c9732f2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 27 Aug 2020 14:36:26 +0200
Subject: [PATCH] Let logical operators accept any scalar type as argument
---
src/kernel_internals/typing/cabs2cil.ml | 12 ++----------
src/kernel_services/ast_queries/cil.ml | 15 +++++++++++++--
src/kernel_services/ast_queries/cil.mli | 11 +++++++++--
.../oracle/keep_logical_operators.res.oracle | 2 +-
4 files changed, 25 insertions(+), 15 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 17cf66913b9..d797b501c14 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7784,11 +7784,7 @@ and doCondExp local_env asconst
end else CEAnd (ce1, ce2))
| CEExp(se1, e1'), CEExp (se2, e2') when
theMachine.useLogicalOperators && isEmpty se1 && isEmpty se2 ->
- CEExp
- (empty,
- new_exp ~loc
- (BinOp(LAnd,
- makeCast e1' intType, makeCast e2' intType, intType)))
+ CEExp (empty, new_exp ~loc (BinOp(LAnd, e1', e2', intType)))
| _ -> CEAnd (ce1, ce2)
end
@@ -7807,11 +7803,7 @@ and doCondExp local_env asconst
end else CEOr (ce1, ce2))
| CEExp (se1, e1'), CEExp (se2, e2') when
theMachine.useLogicalOperators && isEmpty se1 && isEmpty se2 ->
- CEExp
- (empty,
- new_exp ~loc
- (BinOp(LOr,
- makeCast e1' intType, makeCast e2' intType, intType)))
+ CEExp (empty, new_exp ~loc (BinOp(LOr, e1', e2', intType)))
| _ -> CEOr (ce1, ce2)
end
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 544e912ca69..c8bfefe2bac 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3583,11 +3583,13 @@ let isLongDoubleType t =
| TFloat(FLongDouble,_) -> true
| _ -> false
-let isArithmeticOrPointerType t=
+let isScalarType t=
match unrollTypeSkel t with
| TInt _ | TEnum _ | TFloat _ | TPtr _ -> true
| _ -> false
+let isArithmeticOrPointerType = isScalarType
+
let rec isLogicArithmeticType t =
match t with
| Ctype t -> isArithmeticType t
@@ -6186,9 +6188,18 @@ let mkBinOp ~loc op e1 e2 =
in
constFoldBinOp ~loc machdep op e1 e2 intType
in
+ let check_scalar op e t =
+ if not (isScalarType t) then
+ Kernel.fatal ~current:true "operand of %s is not scalar: %a"
+ op !pp_exp_ref e
+ in
match op with
(Mult|Div) -> doArithmetic ()
- | (Mod|BAnd|BOr|BXor|LAnd|LOr) -> doIntegralArithmetic ()
+ | (Mod|BAnd|BOr|BXor) -> doIntegralArithmetic ()
+ | LAnd | LOr ->
+ check_scalar "logical operator" e1 t1;
+ check_scalar "logical operator" e2 t2;
+ constFoldBinOp ~loc machdep op e1 e2 intType
| (Shiftlt|Shiftrt) -> (* ISO 6.5.7. Only integral promotions. The result
* has the same type as the left hand side *)
if msvcMode () then
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 16dae549fb4..b0dcdc46c5e 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -546,8 +546,15 @@ val isLogicRealType: logic_type -> bool
floating point *)
val isArithmeticType: typ -> bool
-(** True if the argument is an arithmetic or pointer type (i.e. integer, enum,
- floating point or pointer *)
+(** True if the argument is a scalar type (i.e. integral, enum,
+ floating point or pointer
+ @since Frama-C+dev
+ *)
+val isScalarType: typ -> bool
+
+(** alias of isScalarType.
+ @deprecated Frama-C+dev use isScalarType instead
+ *)
val isArithmeticOrPointerType: typ -> bool
(** True if the argument is a logic arithmetic type (i.e. integer, enum or
diff --git a/tests/syntax/oracle/keep_logical_operators.res.oracle b/tests/syntax/oracle/keep_logical_operators.res.oracle
index 23aec588134..2bfe2908271 100644
--- a/tests/syntax/oracle/keep_logical_operators.res.oracle
+++ b/tests/syntax/oracle/keep_logical_operators.res.oracle
@@ -14,7 +14,7 @@ int test(int a, int b, int c)
int test_ptr(int *a, int *b, int *c)
{
int __retres;
- if ((int)a && ((int)b || (int)c)) {
+ if (a && (b || c)) {
__retres = 1;
goto return_label;
}
--
GitLab