From 6217c36c4dfba4fafe7a8bebc73f4f5f43e42646 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Fri, 17 Jun 2022 15:06:27 +0200
Subject: [PATCH] [e-acsl] review
---
src/plugins/e-acsl/src/analyses/typing.ml | 67 ++++++++++++++---------
1 file changed, 41 insertions(+), 26 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index e005bcb1db7..bab9f53ab27 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -708,15 +708,21 @@ and number_ty_bound_variable ~profile (t1, lv, t2) =
let i = Interval.(widen (join i1 i2)) in
match lv.lv_type with
| Linteger ->
- (match t2.term_type with
- | Ctype (TInt (ik, _) as typ) when
- Interval.is_included i (Interval.interv_of_typ typ)
- -> mk_ctx ~use_gmp_opt:true (C_integer ik)
- | _ -> (match t2.term_node with
- | TLogic_coerce(_, {term_type = Ctype (TInt (ik, _) as typ)}) when
+ let t2 = Logic_utils.remove_logic_coerce t2 in
+ let ty =
+ match t2.term_type with
+ | Ctype typ ->
+ (match Cil.unrollType typ with
+ | TInt (ik, _) | TEnum({ ekind = ik }, _) when
Interval.is_included i (Interval.interv_of_typ typ)
- -> mk_ctx ~use_gmp_opt:true (C_integer ik)
- | _ -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)))
+ -> Some (C_integer ik)
+ | TInt _ | TEnum _ | TFloat _ | TVoid _ | TPtr _ | TArray _ | TFun _
+ | TComp _ | TBuiltin_va_list _ | TNamed _ -> None)
+ | _ -> 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))
| Ctype ty ->
(match Cil.unrollType ty with
| TInt(ik, _) | TEnum({ ekind = ik}, _)-> join
@@ -839,25 +845,34 @@ and ctx_relation ~profile t1 t2 =
let i1 = Interval.get_from_profile ~profile t1 in
let i2 = Interval.get_from_profile ~profile t2 in
let i = Interval.join i1 i2 in
- match t1.term_type with
- | Ctype (TInt (ik, _) as typ) when
- Interval.is_included i (Interval.interv_of_typ typ)
- -> mk_ctx ~use_gmp_opt:true (C_integer ik)
- | _ ->
+ let t1 = Logic_utils.remove_logic_coerce t1 in
+ let ty1 =
+ match t1.term_type with
+ | Ctype typ ->
+ (match Cil.unrollType typ with
+ | TInt (ik, _) | TEnum({ ekind = ik }, _) when
+ Interval.is_included i (Interval.interv_of_typ typ)
+ -> Some (C_integer ik)
+ | TInt _ | TEnum _ | TFloat _ | TVoid _ | TPtr _ | TArray _ | TFun _
+ | TComp _ | TBuiltin_va_list _ | TNamed _ -> None)
+ | _ -> None
+ in
+ let t2 = Logic_utils.remove_logic_coerce t2 in
+ let ty2 =
match t2.term_type with
- | Ctype (TInt (ik, _) as typ) when
- Interval.is_included i (Interval.interv_of_typ typ)
- -> mk_ctx ~use_gmp_opt:true (C_integer ik)
- | _ -> match t1.term_node with
- | TLogic_coerce(_, {term_type = Ctype (TInt (ik, _) as typ)}) when
- Interval.is_included i (Interval.interv_of_typ typ)
- -> mk_ctx ~use_gmp_opt:true (C_integer ik)
- | _ -> match t2.term_node with
- | TLogic_coerce(_, {term_type = Ctype (TInt (ik, _) as typ)}) when
- Interval.is_included i (Interval.interv_of_typ typ)
- -> mk_ctx ~use_gmp_opt:true (C_integer ik)
- | _ -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i)
-
+ | Ctype typ ->
+ (match Cil.unrollType typ with
+ | TInt (ik, _) | TEnum({ ekind = ik }, _) when
+ Interval.is_included i (Interval.interv_of_typ typ)
+ -> Some (C_integer ik)
+ | TInt _ | TEnum _ | TFloat _ | TVoid _ | TPtr _ | TArray _ | TFun _
+ | TComp _ | TBuiltin_va_list _ | TNamed _ -> None)
+ | _ -> 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 type_term ~use_gmp_opt ?ctx ~profile t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
--
GitLab