diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 09a1cb3bbc09371d93d886c8002f26dcb6e367ca..74c9c3317e95082defef2e5b3d71738fc661dce9 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -7692,17 +7692,22 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) = intType in let doIntegralArithmetic () = - let tres = unrollType (arithmeticConversion t1 t2) in - match tres with - | TInt _ -> - tres, - optConstFoldBinOp loc false bop - (makeCastT ~e:e1 ~oldt:t1 ~newt:tres) - (makeCastT ~e:e2 ~oldt:t2 ~newt:tres) - tres - | _ -> - abort_context "%a operator on non-integer type %a" - Cil_printer.pp_binop bop Cil_datatype.Typ.pretty tres + if isIntegralType t1 && isIntegralType t2 then begin + let tres = unrollType (arithmeticConversion t1 t2) in + match tres with + | TInt _ -> + tres, + optConstFoldBinOp loc false bop + (makeCastT ~e:e1 ~oldt:t1 ~newt:tres) + (makeCastT ~e:e2 ~oldt:t2 ~newt:tres) + tres + | _ -> + Kernel.fatal + "conversion of integer types %a and %a returned a non-integer type %a" + Cil_printer.pp_typ t1 Cil_printer.pp_typ t2 Cil_printer.pp_typ tres + end else + abort_context "%a operator on non-integer type(s) %a and %a" + Cil_printer.pp_binop bop Cil_printer.pp_typ t1 Cil_printer.pp_typ t2 in (* Invariant: t1 and t2 are pointers types *) let pointerComparison e1 t1 e2 t2 = diff --git a/tests/syntax/oracle/binary_op.res.oracle b/tests/syntax/oracle/binary_op.res.oracle index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..c173a17a4888d542864764bd6b2de3ae9cd27a10 100644 --- a/tests/syntax/oracle/binary_op.res.oracle +++ b/tests/syntax/oracle/binary_op.res.oracle @@ -0,0 +1,8 @@ +[kernel] Parsing binary_op.i (no preprocessing) +[kernel] binary_op.i:6: User Error: + & operator on non-integer type(s) int and int (*)(void) + 4 */ + 5 + 6 int v(void) { return 0 & v; } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +[kernel] Frama-C aborted: invalid user input.