diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 74c9c3317e95082defef2e5b3d71738fc661dce9..e2fedba13a469501a094a3d0a87af7e7a9b8da98 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -7674,13 +7674,18 @@ and normalize_binop binop action local_env asconst le re what = * version if necessary *) and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) = let doArithmetic () = - let tres = arithmeticConversion t1 t2 in - (* Keep the operator since it is arithmetic *) - tres, - optConstFoldBinOp loc false bop - (makeCastT ~e:e1 ~oldt:t1 ~newt:tres) - (makeCastT ~e:e2 ~oldt:t2 ~newt:tres) - tres + if isArithmeticType t1 && isArithmeticType t2 then begin + let tres = arithmeticConversion t1 t2 in + (* Keep the operator since it is arithmetic *) + tres, + optConstFoldBinOp loc false bop + (makeCastT ~e:e1 ~oldt:t1 ~newt:tres) + (makeCastT ~e:e2 ~oldt:t2 ~newt:tres) + tres + end else + abort_context + "%a operator on non-arithmetic type(s) %a and %a" + Cil_printer.pp_binop bop Cil_printer.pp_typ t1 Cil_printer.pp_typ t2 in let doArithmeticComp () = let tres = arithmeticConversion t1 t2 in diff --git a/tests/syntax/binary_op.c b/tests/syntax/binary_op.c new file mode 100644 index 0000000000000000000000000000000000000000..da6c970aca02427d113d6cc3da3e3348af6548ca --- /dev/null +++ b/tests/syntax/binary_op.c @@ -0,0 +1,24 @@ +/* run.config +EXIT: 1 +OPT:-cpp-extra-args="-DBITWISE" +OPT:-cpp-extra-args="-DMULT" +EXIT: 0 +OPT:-cpp-extra-args="-DADD" +OPT:-cpp-extra-args="-DCMP" +*/ + +#ifdef BITWISE +int v(void) { return 0 & v; } +#endif + +#ifdef MULT +int w(void) { return 0 * w; } +#endif + +#ifdef ADD +int x(void) { return 0 + x; } +#endif + +#ifdef CMP +int y(void) { return 0 <= y; } +#endif diff --git a/tests/syntax/binary_op.i b/tests/syntax/binary_op.i deleted file mode 100644 index 768af5955de4c0cfbedb856b264773cb3bc8fb71..0000000000000000000000000000000000000000 --- a/tests/syntax/binary_op.i +++ /dev/null @@ -1,6 +0,0 @@ -/* run.config -EXIT: 1 -STDOPT: -*/ - -int v(void) { return 0 & v; } diff --git a/tests/syntax/oracle/binary_op.0.res.oracle b/tests/syntax/oracle/binary_op.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..60dc2afc775623a14bdbf16138e62b32b11d1e61 --- /dev/null +++ b/tests/syntax/oracle/binary_op.0.res.oracle @@ -0,0 +1,10 @@ +[kernel] Parsing binary_op.c (with preprocessing) +[kernel] binary_op.c:11: User Error: + & operator on non-integer type(s) int and int (*)(void) + 9 + 10 #ifdef BITWISE + 11 int v(void) { return 0 & v; } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + 12 #endif + 13 +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/binary_op.1.res.oracle b/tests/syntax/oracle/binary_op.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..b896f4027b9e1e78d89cc8d7ee7d295179e244cb --- /dev/null +++ b/tests/syntax/oracle/binary_op.1.res.oracle @@ -0,0 +1,10 @@ +[kernel] Parsing binary_op.c (with preprocessing) +[kernel] binary_op.c:15: User Error: + * operator on non-arithmetic type(s) int and int (*)(void) + 13 + 14 #ifdef MULT + 15 int w(void) { return 0 * w; } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + 16 #endif + 17 +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/binary_op.2.res.oracle b/tests/syntax/oracle/binary_op.2.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..b60a0b2353c7adfc2e6d79127480eb82a96e7536 --- /dev/null +++ b/tests/syntax/oracle/binary_op.2.res.oracle @@ -0,0 +1,3 @@ +[kernel] Parsing binary_op.c (with preprocessing) +[kernel:typing:int-conversion] binary_op.c:19: Warning: + Conversion from a pointer to an integer without an explicit cast diff --git a/tests/syntax/oracle/binary_op.3.res.oracle b/tests/syntax/oracle/binary_op.3.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..651bbbc78159bd4e23ed58294aaa84bc2c5485bd --- /dev/null +++ b/tests/syntax/oracle/binary_op.3.res.oracle @@ -0,0 +1 @@ +[kernel] Parsing binary_op.c (with preprocessing) diff --git a/tests/syntax/oracle/binary_op.res.oracle b/tests/syntax/oracle/binary_op.res.oracle deleted file mode 100644 index c173a17a4888d542864764bd6b2de3ae9cd27a10..0000000000000000000000000000000000000000 --- a/tests/syntax/oracle/binary_op.res.oracle +++ /dev/null @@ -1,8 +0,0 @@ -[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.