diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 6c67279044..0a850b03a3 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2074,10 +2074,22 @@ struct | _ -> None let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L)) - let of_interval ?(suppress_ovwarn=false) ik (x,y) = if Z.compare x y = 0 then of_int ik x else top_of ik + let of_interval ?(suppress_ovwarn=false) ik (x,y) = + if Z.compare x y = 0 then + of_int ik x + else + let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in + let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval ~suppress_ovwarn range_ikind b) in + let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in + norm ik @@ (`Excluded (ex, r)) + + let starting ?(suppress_ovwarn=false) ikind x = + let _,u_ik = Size.range ikind in + of_interval ~suppress_ovwarn ikind (x, u_ik) - let starting ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero > 0 then not_zero ikind else top_of ikind - let ending ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero < 0 then not_zero ikind else top_of ikind + let ending ?(suppress_ovwarn=false) ikind x = + let l_ik,_ = Size.range ikind in + of_interval ~suppress_ovwarn ikind (l_ik, x) let of_excl_list t l = let r = size t in (* elements in l are excluded from the full range of t! *) @@ -2491,7 +2503,14 @@ module Enums : S with type int_t = Z.t = struct let of_int ikind x = cast_to ikind (Inc (BISet.singleton x)) - let of_interval ?(suppress_ovwarn=false) ik (x,y) = if x = y then of_int ik x else top_of ik + let of_interval ?(suppress_ovwarn=false) ik (x, y) = + if Z.compare x y = 0 then + of_int ik x + else + let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in + let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval ~suppress_ovwarn range_ikind b) in + let ex = if Z.gt x Z.zero || Z.lt y Z.zero then BISet.singleton Z.zero else BISet.empty () in + norm ik @@ (Exc (ex, r)) let join ik = curry @@ function | Inc x, Inc y -> Inc (BISet.union x y) @@ -2626,8 +2645,13 @@ module Enums : S with type int_t = Z.t = struct let is_excl_list = BatOption.is_some % to_excl_list let to_incl_list = function Inc s when not (BISet.is_empty s) -> Some (BISet.elements s) | _ -> None - let starting ?(suppress_ovwarn=false) ikind x = top_of ikind - let ending ?(suppress_ovwarn=false) ikind x = top_of ikind + let starting ?(suppress_ovwarn=false) ikind x = + let _,u_ik = Size.range ikind in + of_interval ~suppress_ovwarn ikind (x, u_ik) + + let ending ?(suppress_ovwarn=false) ikind x = + let l_ik,_ = Size.range ikind in + of_interval ~suppress_ovwarn ikind (l_ik, x) let c_lognot ik x = if is_bot x diff --git a/tests/regression/01-cpa/75-refine-def-exc.c b/tests/regression/01-cpa/75-refine-def-exc.c new file mode 100644 index 0000000000..244ec986b1 --- /dev/null +++ b/tests/regression/01-cpa/75-refine-def-exc.c @@ -0,0 +1,16 @@ +//PARAM: --enable ana.int.def_exc --disable ana.int.interval +#include +#include +#include + +int main () { + // Needs to be unsigned as we create ranges corresponding to types and ending for signed + // means we have int as there are no types containing only negative numbers + unsigned int r; + + if(r < 1024) { + __goblint_check(r <= 32768); + } + + return 0; +} diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index 705fb8d497..02f6c1e5e0 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -67,7 +67,7 @@ total lines: 6 [Warning][Deadcode][CWE-571] condition 'a > 0' (possibly inserted by CIL) is always true (foo.c:3:10-3:20) [Info][Witness] witness generation summary: - total generation entries: 13 + total generation entries: 15 $ yamlWitnessStrip < witness.yml - entry_type: loop_invariant @@ -125,6 +125,17 @@ string: 1 <= a type: assertion format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 7 + column: 3 + function: main + location_invariant: + string: 0 <= a + type: assertion + format: C - entry_type: location_invariant location: file_name: foo.c @@ -213,3 +224,14 @@ string: 1 <= a type: assertion format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 5 + function: main + location_invariant: + string: 0 <= a + type: assertion + format: C