From af4ad89054b851a3bed38977400c48f9b1c51b28 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 1 Apr 2020 10:19:24 +0200
Subject: [PATCH] [kernel] also coerce enum constants
---
.../ast_queries/logic_utils.ml | 21 +++++++++----------
.../oracle/enum.res.oracle | 4 ++--
.../oracle/cast_enum_bts1546.0.res.oracle | 2 +-
3 files changed, 13 insertions(+), 14 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index c08f9d6d6ae..9f0a5c558d9 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -227,13 +227,6 @@ let equal_ltype = Cil_datatype.Logic_type.equal
let mk_cast ?loc ?(force=false) newt t =
let newt = Cil.type_remove_attributes_for_logic_type newt in
if equal_ltype (Ctype newt) t.term_type then t else
- (*
- let rec is_iconst e = match e.term_node with
- | TCastE(ty,e) when Cil.isArithmeticOrPointerType ty -> is_iconst e
- | TLogic_coerce(Linteger,e) -> is_iconst e
- | TConst(Integer _) -> true
- | _ -> false in
- *)
let rec unroll_cast e = match e.term_node with
| TCastE(oldt,e)
when (Cil.isPointerType newt && Cil.isPointerType oldt)
@@ -248,8 +241,8 @@ let mk_cast ?loc ?(force=false) newt t =
| _ -> e
in
let tres = if force then t else unroll_cast t in
- let loc = match loc with None -> t.term_loc | Some loc -> loc in
- Logic_const.term ~loc (TCastE (newt, tres)) (Ctype newt)
+ let loc = match loc with None -> t.term_loc | Some loc -> loc in
+ Logic_const.term ~loc (TCastE (newt, tres)) (Ctype newt)
(* -------------------------------------------------------------------------- *)
@@ -319,14 +312,20 @@ let numeric_coerce ltyp t =
| TLogic_coerce(lt,e) when Cil.no_op_coerce lt e ->
(* coercion hidden by the printer, but still present *)
mk_coerce ltyp e
- | TConst(Integer _) when ltyp = Linteger -> { t with term_type = Linteger }
- | TConst(LReal _ ) when ltyp = Lreal -> { t with term_type = Lreal }
+ | TConst(LEnum _) | TConst(Integer _) when ltyp = Linteger
+ -> { t with term_type = Linteger }
+ | TConst(LReal _ ) when ltyp = Lreal ->
+ { t with term_type = Lreal }
| TCastE(ty,e) ->
begin match ltyp, Cil.unrollType ty, e.term_node with
| Linteger, TInt(ik,_), TConst(Integer(v,_))
when Cil.fitsInInt ik v -> { e with term_type = Linteger }
| Lreal, TFloat(fk,_), TConst(LReal r)
when Cil.isFiniteFloat fk r.r_nearest -> { e with term_type = Lreal }
+ | Linteger, TInt(ik,_), TConst(LEnum { eival }) ->
+ ( match Cil.constFoldToInt eival with
+ | Some i when Cil.fitsInInt ik i -> { e with term_type = Linteger }
+ | _ -> mk_coerce ltyp t )
| _ -> mk_coerce ltyp t
end
| _ -> mk_coerce ltyp t
diff --git a/tests/constant_propagation/oracle/enum.res.oracle b/tests/constant_propagation/oracle/enum.res.oracle
index d7c4e9f6ea0..cbd71cd5823 100644
--- a/tests/constant_propagation/oracle/enum.res.oracle
+++ b/tests/constant_propagation/oracle/enum.res.oracle
@@ -14,7 +14,7 @@
[eva] Recording results for f
[eva] Done for function f
[eva:alarm] tests/constant_propagation/enum.i:13: Warning:
- signed overflow. assert (int)B + c ≤ 2147483647;
+ signed overflow. assert B + c ≤ 2147483647;
[eva:alarm] tests/constant_propagation/enum.i:15: Warning:
signed overflow. assert (int)(y + z) + t ≤ 2147483647;
[eva:alarm] tests/constant_propagation/enum.i:15: Warning:
@@ -43,7 +43,7 @@ int main(int c, unsigned int u)
enum E x = A;
int y = f(0U);
int z = f(D);
- /*@ assert Eva: signed_overflow: (int)B + c ≤ 2147483647; */
+ /*@ assert Eva: signed_overflow: B + c ≤ 2147483647; */
int t = B + c;
int v = (int)(2U + u);
/*@ assert Eva: signed_overflow: (int)(y + z) + t ≤ 2147483647; */
diff --git a/tests/spec/oracle/cast_enum_bts1546.0.res.oracle b/tests/spec/oracle/cast_enum_bts1546.0.res.oracle
index 859426aa635..8a5f937eecd 100644
--- a/tests/spec/oracle/cast_enum_bts1546.0.res.oracle
+++ b/tests/spec/oracle/cast_enum_bts1546.0.res.oracle
@@ -39,7 +39,7 @@ enum e f(enum e x)
return __retres;
}
-/*@ ensures P: \result ≡ (unsigned int)E0; */
+/*@ ensures P: \result ≡ E0; */
enum e g(enum e x)
{
enum e __retres;
--
GitLab