Merge pull request #2022 from goblint/reach-oob-checks

Disable OOB checks during reachability calculations

Author: sim642

src/analyses/base.ml

@@ -613,10 +613,15 @@ struct
     | JmpBuf _ -> empty (* Jump buffers are abstract and nothing known can be reached from them *)
     | Mutex -> empty (* mutexes are abstract and nothing known can be reached from them *)
 
+  let reachable_from_value ask (value: value) (t: typ) (description: string) =
+    let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+    reachable_from_value ask value t description
+
   (* Get the list of addresses accessible immediately from a given address, thus
    * all pointers within a structure should be considered, but we don't follow
    * pointers. We return a flattend representation, thus simply an address (set). *)
   let reachable_from_addr ~man st (addr: Addr.t): address =
+    let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
     if M.tracing then M.tracei "reachability" "Checking for %a" Addr.pretty addr;
     let res = reachable_from_value (Analyses.ask_of_man man) (get_addr ~man st addr None) (Addr.type_of addr) (Addr.show addr) in
     if M.tracing then M.traceu "reachability" "Reachable addresses: %a" AD.pretty res;
@@ -696,6 +701,7 @@ struct
 
 
   let reachable_top_pointers_types man (ps: AD.t) : Queries.TS.t =
+    let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
     let module TS = Queries.TS in
     let empty = AD.empty () in
     let reachable_from_address (adr: address) =

src/cdomain/value/cdomains/arrayDomain.ml

@@ -802,7 +802,9 @@ end
 
 (* This is the main array out of bounds check *)
 let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) =
-  if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
+  if !AnalysisState.executing_speculative_computations then
+    ()
+  else if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
     let idx_before_end = Idx.lt v l in (* check whether index is before the end of the array *)
     let idx_after_start = Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) in (* check whether the index is non-negative *)
     (* For an explanation of the warning types check the Pull Request #255 *)

tests/regression/25-vla/07-zero-arg-reach.c

@@ -0,0 +1,16 @@
+// PARAM: --enable ana.arrayoob
+// extracted from SV-COMP task ldv-memsafety/ArraysOfVariableLength2.c
+
+int bar(int b[]) {
+  return 0;
+}
+
+void foo(int n) {
+  int a[n];
+  bar(a); //NOWARN
+}
+
+int main(void) {
+  foo(0);
+  return 0;
+}