diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 0a59dd7ea6ba6a9a85bf4300dd8a304a1d7995ee..de0e67072492daa5af65815d4cff643da90a7455 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1349,15 +1349,19 @@ let makeCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) = let makeCast ~(e: exp) ~(newt: typ) = makeCastT e (typeOf e) newt -(* A cast that is used for conditional expressions. Pointers are Ok. - Abort if invalid *) -let checkBool (ot : typ) (_ : exp) = - match unrollType ot with +let is_scalar_type t = + match unrollType t with | TInt _ | TPtr _ | TEnum _ - | TFloat _ -> () - | _ -> Kernel.fatal ~current:true "castToBool %a" Cil_printer.pp_typ ot + | TFloat _ -> true + | _ -> false + +(* A cast that is used for conditional expressions. Pointers are Ok. + Abort if invalid *) +let checkBool (ot : typ) (_ : exp) = + if not (is_scalar_type ot) then + Kernel.fatal ~current:true "castToBool %a" Cil_printer.pp_typ ot (* Evaluate constants to CTrue (non-zero) or CFalse (zero) *) let rec isConstTrueFalse c: [ `CTrue | `CFalse ] = @@ -2838,7 +2842,7 @@ let rec castTo ?context ?(fromsource=false) match ot', nt' with | TNamed _, _ | _, TNamed _ -> Kernel.fatal ~current:true "unrollType failed in castTo" - | _, TInt(IBool,_) -> + | t, TInt(IBool,_) when is_scalar_type t -> if is_boolean_result e then result else nt, diff --git a/tests/syntax/oracle/wrong-assignment.res.oracle b/tests/syntax/oracle/wrong-assignment.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..aba1a2ecee9a40e229449d6158e269eae7c2061f --- /dev/null +++ b/tests/syntax/oracle/wrong-assignment.res.oracle @@ -0,0 +1,4 @@ +[kernel] Parsing tests/syntax/wrong-assignment.i (no preprocessing) +[kernel] tests/syntax/wrong-assignment.i:7: Failure: castTo ebool -> _Bool +[kernel] User Error: stopping on file "tests/syntax/wrong-assignment.i" that has errors. +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/wrong-assignment.i b/tests/syntax/wrong-assignment.i new file mode 100644 index 0000000000000000000000000000000000000000..da2a59b86aef70d1ce5cf3732635f24f7f810883 --- /dev/null +++ b/tests/syntax/wrong-assignment.i @@ -0,0 +1,8 @@ +typedef struct { _Bool a; } ebool; + +ebool b, c; + +void d() { + // this assignment should be rejected + c.a = b; +}