From 28005751b0e240ff20c923cd718d546277d11a6b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 6 Sep 2023 10:38:23 +0200
Subject: [PATCH] [kernel] dot not crash on ill-typed bitwise operators
---
src/kernel_internals/typing/cabs2cil.ml | 27 ++++++++++++++----------
tests/syntax/oracle/binary_op.res.oracle | 8 +++++++
2 files changed, 24 insertions(+), 11 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 09a1cb3bbc0..74c9c3317e9 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 e69de29bb2d..c173a17a488 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.
--
GitLab