From 7199ab95d9cd50e2df31149d1185bd785d7fd45c Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Fri, 17 Jun 2022 15:48:06 +0200
Subject: [PATCH] [e-acsl] review
---
src/plugins/e-acsl/src/analyses/typing.ml | 44 +++++++++++++------
.../e-acsl/tests/arith/oracle/gen_let.c | 3 +-
2 files changed, 31 insertions(+), 16 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index bab9f53ab27..6f542b69e24 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -715,14 +715,20 @@ and number_ty_bound_variable ~profile (t1, lv, t2) =
(match Cil.unrollType typ with
| TInt (ik, _) | TEnum({ ekind = ik }, _) when
Interval.is_included i (Interval.interv_of_typ typ)
- -> Some (C_integer ik)
+ ->
+ if Cil.intTypeIncluded ik IInt
+ then Some (C_integer IInt)
+ else Some (C_integer ik)
| TInt _ | TEnum _ | TFloat _ | TVoid _ | TPtr _ | TArray _ | TFun _
- | TComp _ | TBuiltin_va_list _ | TNamed _ -> None)
+ | TComp _ | TBuiltin_va_list _ -> None
+ | TNamed _ -> assert false)
| _ -> None
in
- (match ty with
- | Some ty -> mk_ctx ~use_gmp_opt:true ty
- | None -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i))
+ let ty =
+ match ty with
+ | Some ty -> ty
+ | None -> ty_of_interv ~ctx:Gmpz i
+ in mk_ctx ~use_gmp_opt:true ty
| Ctype ty ->
(match Cil.unrollType ty with
| TInt(ik, _) | TEnum({ ekind = ik}, _)-> join
@@ -839,7 +845,7 @@ and type_predicate ~profile p =
should be typed, to avoid spurious casts:
- Compute the union of the interval of the two terms
- Check if any of the term has a number C type that contains this union,
- and if so use this C type
+ and if so use this C type, or [int] if this type is smaller than [int]
- Otherwise use the type corresponding to the union *)
and ctx_relation ~profile t1 t2 =
let i1 = Interval.get_from_profile ~profile t1 in
@@ -852,9 +858,13 @@ and ctx_relation ~profile t1 t2 =
(match Cil.unrollType typ with
| TInt (ik, _) | TEnum({ ekind = ik }, _) when
Interval.is_included i (Interval.interv_of_typ typ)
- -> Some (C_integer ik)
+ ->
+ if Cil.intTypeIncluded ik IInt
+ then Some (C_integer IInt)
+ else Some (C_integer ik)
| TInt _ | TEnum _ | TFloat _ | TVoid _ | TPtr _ | TArray _ | TFun _
- | TComp _ | TBuiltin_va_list _ | TNamed _ -> None)
+ | TComp _ | TBuiltin_va_list _ -> None
+ | TNamed _ -> assert false)
| _ -> None
in
let t2 = Logic_utils.remove_logic_coerce t2 in
@@ -864,15 +874,21 @@ and ctx_relation ~profile t1 t2 =
(match Cil.unrollType typ with
| TInt (ik, _) | TEnum({ ekind = ik }, _) when
Interval.is_included i (Interval.interv_of_typ typ)
- -> Some (C_integer ik)
+ ->
+ if Cil.intTypeIncluded ik IInt
+ then Some (C_integer IInt)
+ else Some (C_integer ik)
| TInt _ | TEnum _ | TFloat _ | TVoid _ | TPtr _ | TArray _ | TFun _
- | TComp _ | TBuiltin_va_list _ | TNamed _ -> None)
+ | TComp _ | TBuiltin_va_list _ -> None
+ | TNamed _ -> assert false)
| _ -> None
in
- match ty1, ty2 with
- | Some ty, _
- | None, Some ty -> mk_ctx ~use_gmp_opt:true ty
- | None, None -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i)
+ let ty =
+ match ty1, ty2 with
+ | Some ty, _
+ | None, Some ty -> ty
+ | None, None -> ty_of_interv ~ctx:c_int i
+ in mk_ctx ~use_gmp_opt:true ty
let type_term ~use_gmp_opt ?ctx ~profile t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_let.c b/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
index 99df90ac494..6c66e98c732 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
@@ -174,8 +174,7 @@ int main(void)
__gen_e_acsl_assert_data_7.file = "let.c";
__gen_e_acsl_assert_data_7.fct = "main";
__gen_e_acsl_assert_data_7.line = 27;
- __e_acsl_assert((int)c < (int)((char)__gen_e_acsl_u_9),
- & __gen_e_acsl_assert_data_7);
+ __e_acsl_assert((int)c < __gen_e_acsl_u_9,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
}
/*@ assert \let u = 'b'; c < u; */ ;
--
GitLab