remove checkbounds for reachable_from -> leads to warnings in the wro…

…ng line of code
goblint · Feb 9, 2024 · ab38192 · ab38192
1 parent 361f5bc
commit ab38192
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git 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
@@ -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);
 }