From e57504b7e2eb07f184ee4459a325fad7cb731eef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 1 Apr 2020 16:53:23 +0200
Subject: [PATCH] [kernel] preserve original types in expr-to-term
---
src/kernel_services/ast_queries/logic_utils.ml | 16 +++++++++-------
tests/rte/oracle/addsub_typedef.res.oracle | 3 ++-
tests/rte/oracle/divmod_typedef.res.oracle | 2 +-
3 files changed, 12 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 859f27b27ac..d1bcc167969 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -404,7 +404,7 @@ let float_builtin prefix fkind =
| _ -> Kernel.fatal "Missing or ambiguous builtin %S" name
let get_float_binop op typ =
- match typ, op with
+ match Cil.unrollType typ, op with
| TFloat(fkind,_) , PlusA -> float_builtin "add" fkind
| TFloat(fkind,_) , MinusA -> float_builtin "sub" fkind
| TFloat(fkind,_) , Mult -> float_builtin "mul" fkind
@@ -412,13 +412,13 @@ let get_float_binop op typ =
| _ -> None
let get_float_unop op typ =
- match typ, op with
+ match Cil.unrollType typ, op with
| TFloat(fkind,_) , Neg -> float_builtin "neg" fkind
| _ -> None
let rec expr_to_term ?(coerce=false) e =
let loc = e.eloc in
- let typ = Cil.unrollType (Cil.typeOf e) in
+ let typ = Cil.typeOf e in
let ctyp = Ctype typ in
let node,ltyp =
match e.enode with
@@ -468,10 +468,12 @@ let rec expr_to_term ?(coerce=false) e =
t.term_node , t.term_type
in
let v = mk_cast ~loc typ @@ Logic_const.term ~loc node ltyp in
- match typ with
- | TInt _ when coerce -> numeric_coerce Linteger v
- | TFloat _ when coerce -> numeric_coerce Lreal v
- | _ -> v
+ if coerce then
+ match Cil.unrollType typ with
+ | TInt _ -> numeric_coerce Linteger v
+ | TFloat _ -> numeric_coerce Lreal v
+ | _ -> v
+ else v
and lval_to_term_lval (host,offset) =
host_to_term_lhost host, offset_to_term_offset offset
diff --git a/tests/rte/oracle/addsub_typedef.res.oracle b/tests/rte/oracle/addsub_typedef.res.oracle
index adf710ee1ac..8e0232c30ba 100644
--- a/tests/rte/oracle/addsub_typedef.res.oracle
+++ b/tests/rte/oracle/addsub_typedef.res.oracle
@@ -41,7 +41,8 @@ int main(void)
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-0x7ffffffc) - y; */
z = -0x7ffffffc - y;
/*@ assert rte: signed_overflow: -2147483647 ≤ x; */
- /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-x) - 0x7ffffffc; */
+ /*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-x) - 0x7ffffffc;
+ */
z = - x - 0x7ffffffc;
/*@ assert rte: signed_overflow: 0x7ffffffc + y ≤ 2147483647; */
z = 0x7ffffffc + y;
diff --git a/tests/rte/oracle/divmod_typedef.res.oracle b/tests/rte/oracle/divmod_typedef.res.oracle
index 51b06e5796e..a965ff5054d 100644
--- a/tests/rte/oracle/divmod_typedef.res.oracle
+++ b/tests/rte/oracle/divmod_typedef.res.oracle
@@ -65,7 +65,7 @@ int main(void)
uz = (unsigned int)((int)(0x80000000 / 0xffffffff));
/*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */
/*@ assert rte: signed_overflow: x + y ≤ 2147483647; */
- /*@ assert rte: division_by_zero: (int)(x + y) ≢ 0; */
+ /*@ assert rte: division_by_zero: (tint)(x + y) ≢ 0; */
z = 1 / (x + y);
/*@ assert rte: signed_overflow: x / (int)(-1) ≤ 2147483647; */
z = x / -1;
--
GitLab