From 40b34346ff77e078a29dbaef2d195fe552402e86 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 30 Jul 2024 11:04:28 +0300 Subject: [PATCH] Add TODOs about IntDomain refinement --- src/cdomain/value/cdomains/intDomain.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 2d40e6a161..c983e543fa 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2794,7 +2794,7 @@ module Enums : S with type int_t = Z.t = struct | Inc e, Some (c, m) -> Inc (BISet.filter (contains c m) e) | _ -> a - let refine_with_interval ik a b = a + let refine_with_interval ik a b = a (* TODO: refine inclusion (exclusion?) set *) let refine_with_excl_list ik a b = match b with @@ -3577,7 +3577,7 @@ module IntDomTupleImpl = struct in [(fun (a, b, c, d, e) -> refine_with_excl_list ik (a, b, c, d, e) (to_excl_list (a, b, c, d, e))); (fun (a, b, c, d, e) -> refine_with_incl_list ik (a, b, c, d, e) (to_incl_list (a, b, c, d, e))); - (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b); + (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b); (* TODO: get interval across all domains with minimal and maximal *) (fun (a, b, c, d, e) -> maybe refine_with_congruence ik (a, b, c, d, e) d)] let refine ik ((a, b, c, d, e) : t ) : t = @@ -3791,6 +3791,7 @@ module IntDomTupleImpl = struct | _ -> BatPrintf.fprintf f "\n\n%s\n\n\n" (show x) let invariant_ikind e ik ((_, _, _, x_cong, x_intset) as x) = + (* TODO: do refinement before to ensure incl_list being more precise than intervals, etc (https://github.com/goblint/analyzer/pull/1517#discussion_r1693998515), requires refine functions to actually refine that *) let simplify_int fallback = match to_int x with | Some v ->