diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 17cf66913b9a127047fe7e66bbaf98ad4e871dfb..d797b501c14997fe7e4e37b9ec7721a4be551aa3 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 544e912ca692472f847d2aa060ffd96c604f2c19..6448005f8a5aeb68f557acfd7bb5ef6507445678 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 16dae549fb4dd7a16f26e3e882bc34b7cc5967c9..64a5b55a779e982ac5e1cd44d0269eaff07d47c4 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/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index c9dae9c7fd2a8eb422b6976f2bce1c8bf15cf982..1a79a063bcccf19f424e65cd849fe2f881c7f838 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -371,7 +371,7 @@ module UnrollingForce: Parameter_sig.Bool called for well preparing the AST. *) module Machdep: Parameter_sig.String -(** Behavior of invisible option -keep-logical operator: +(** Behavior of invisible option -keep-logical-operators: Tries to avoid converting && and || into conditional statements. Note that this option is incompatible with many (most) plug-ins of the platform and thus should only be enabled with great care and for very diff --git a/tests/syntax/keep_logical_operators.i b/tests/syntax/keep_logical_operators.i index dd05ac45a1b8248ca184a8f2f613b7cc86c17bd9..5f7901e2354bbae4862204d9d79ba3abc49e044d 100644 --- a/tests/syntax/keep_logical_operators.i +++ b/tests/syntax/keep_logical_operators.i @@ -9,3 +9,13 @@ int test(int a, int b, int c) { return 2; } + +int test_ptr(int* a, int* b, int* c) { + if (a && (b || c)) { + return 1; + } + if (a) + if (b) + return 2; + return 3; +} diff --git a/tests/syntax/oracle/keep_logical_operators.res.oracle b/tests/syntax/oracle/keep_logical_operators.res.oracle index 99261e5e4c556aee8b36123f86d1860c3680b298..2bfe2908271a7891c4bc6d0e497dd1c9871d9fb6 100644 --- a/tests/syntax/oracle/keep_logical_operators.res.oracle +++ b/tests/syntax/oracle/keep_logical_operators.res.oracle @@ -11,4 +11,20 @@ int test(int a, int b, int c) return_label: return __retres; } +int test_ptr(int *a, int *b, int *c) +{ + int __retres; + if (a && (b || c)) { + __retres = 1; + goto return_label; + } + if (a) + if (b) { + __retres = 2; + goto return_label; + } + __retres = 3; + return_label: return __retres; +} +