From a2ea689339eb19486a582bdfe8e8da8fe67cd3fb Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 31 Jan 2022 10:41:38 +0100
Subject: [PATCH] [kernel] Better error messages for Cil.mkBinOp
---
src/kernel_services/ast_queries/cil.ml | 13 +++++++++++--
1 file changed, 11 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index daae7bfac54..448ed28deb3 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5891,7 +5891,11 @@ let mkBinOp ~loc op e1 e2 =
if isIntegralType tres then
make_expr tres tres
else
- Kernel.fatal ~current:true "mkBinOp: %a" !pp_exp_ref (dummy_exp(BinOp(op,e1,e2,intType)))
+ Kernel.fatal
+ ~current:true
+ "@[mkBinOp: unsupported non integral result type for integral \
+ arithmetic@ %a@]"
+ !pp_exp_ref (dummy_exp(BinOp(op,e1,e2,intType)))
in
let compare_pointer op ?cast1 ?cast2 e1 e2 =
let do_cast e = function
@@ -5952,8 +5956,13 @@ let mkBinOp ~loc op e1 e2 =
compare_pointer ~cast1:theMachine.upointType ~cast2:theMachine.upointType
op e1 e2
| _ ->
- Kernel.fatal ~current:true "mkBinOp: %a"
+ Kernel.fatal
+ ~current:true
+ "@[mkBinOp: unsupported operator for such operands@ \
+ %a@ (type of e1: %a,@ type of e2: %a)@]"
!pp_exp_ref (dummy_exp(BinOp(op,e1,e2,intType)))
+ !pp_typ_ref t1
+ !pp_typ_ref t2
let mkBinOp_safe_ptr_cmp ~loc op e1 e2 =
let e1, e2 =
--
GitLab