diff --git a/src/analyses/base.ml b/src/analyses/base.ml index dcc698ffe76..27a2cd77f35 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -525,7 +525,7 @@ struct | Union (f,e) -> reachable_from_value ask e t description (* For arrays, we ask to read from an unknown index, this will cause it * join all its values. *) - | Array a -> reachable_from_value ask (ValueDomain.CArrays.get (Queries.to_value_domain_ask ask) a (None, ValueDomain.ArrIdxDomain.top ()) None) t description + | Array a -> reachable_from_value ask (ValueDomain.CArrays.get ~checkBounds:false (Queries.to_value_domain_ask ask) a (None, ValueDomain.ArrIdxDomain.top ()) None) t description | Blob (e,_,_) -> reachable_from_value ask e t description | Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask v t description) acc) s empty | Int _ -> empty diff --git a/tests/regression/85-relational-malloc/15-cyclic.c b/tests/regression/85-relational-malloc/15-cyclic.c index 87bbf266bc7..f1b204f394d 100644 --- a/tests/regression/85-relational-malloc/15-cyclic.c +++ b/tests/regression/85-relational-malloc/15-cyclic.c @@ -30,7 +30,16 @@ void foo1(int c) { } void foo2(int c) { + for (int i = 0; i < len; i++) + { + gptr[i] = 42; // NOWARN + gptr[i + 1] = 42; // WARN + gptr[i - 1] = 42; // WARN + int tmp = gptr[i]; // NOWARN + int tmp2 = gptr[i + 1]; // WARN + int tmp3 = gptr[i - 1]; // WARN + } if (c < 10) foo1(c + 1); }