fix Nooverflow computation recursive calls

src/analyses/base.ml

@@ -97,6 +97,9 @@ struct
   module VarMap = Map.Make(CilType.Varinfo)
   let array_map = ref (VarH.create 20)
 
+  (*This is a bit of hack to check if we are currently in a NoOverflow query*)
+  let noOverflow_query_already_started = ref false
+
   type marshal = attributes VarMap.t VarH.t
 
   let array_domain_annotation_enabled = lazy (GobConfig.get_bool "annotation.goblint_array_domain")
@@ -1398,16 +1401,28 @@ struct
       let g: V.t = Obj.obj g in
       query_invariant_global ctx g
     | Q.NoOverflow e ->  
-      MCP.lookUpCache := false;
-      IntDomain.local_no_overflow := true;
-      if M.tracing then M.trace "no_ov" "exp %a\n" d_exp e;
-      let res = try 
-          ignore(query_evalint ~ctx ctx.local  e);
-          !IntDomain.local_no_overflow 
-        with IntDomain.ArithmeticOnIntegerBot _ -> false
-      in
-      MCP.lookUpCache := true;
-      res
+      (* NoOverflow calls EvalInt, which in turn can call NoOverflow again in the relational domain *)
+      if not !noOverflow_query_already_started then (
+        noOverflow_query_already_started := true;
+        IntDomain.local_no_overflow := true;
+        MCP.lookUpCache := false; (*disable caching to compute the [!Intdomain.local_no_overflow] correctly*)
+        let res = try 
+            ignore(query_evalint ~ctx ctx.local  e);
+            !IntDomain.local_no_overflow 
+          with IntDomain.ArithmeticOnIntegerBot _ -> false
+        in
+        MCP.lookUpCache := true;
+        noOverflow_query_already_started := false;
+        res
+      )else 
+      if not !IntDomain.local_no_overflow  then false 
+      else 
+        let res = try 
+            ignore(query_evalint ~ctx ctx.local  e);
+            !IntDomain.local_no_overflow 
+          with IntDomain.ArithmeticOnIntegerBot _ -> false
+        in
+        res
     | _ -> Q.Result.top q
 
   let update_variable variable typ value cpa =

src/cdomain/value/cdomains/intDomain.ml

@@ -80,10 +80,12 @@ let set_overflow_flag ~cast ~underflow ~overflow ik =
   if !AnalysisState.postsolving && signed && not cast then
     AnalysisState.svcomp_may_overflow := true;
   let sign = if signed then "Signed" else "Unsigned" in
+  if M.tracing then M.trace "no_ov" "set = %b\n" !local_no_overflow;
   (if signed && not (get_string "sem.int.signed_overflow" = "assume_none") then
      local_no_overflow := false
-   else 
+   else if not signed then
      local_no_overflow := false);
+  if M.tracing then M.trace "no_ov" "set = %b\n" !local_no_overflow;
   match underflow, overflow with
   | true, true ->
     M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190; CWE 191] "%s integer overflow and underflow" sign

src/domains/queries.ml

@@ -512,7 +512,7 @@ struct
     | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
     | Any (MayBeOutOfBounds x) -> Pretty.dprintf "MayBeOutOfBounds _"
-    | Any (NoOverflow e) -> Pretty.dprintf "MayOverflow %a" CilType.Exp.pretty e
+    | Any (NoOverflow e) -> Pretty.dprintf "NoOverflow %a" CilType.Exp.pretty e
     | Any (AllocMayBeOutOfBounds x) -> Pretty.dprintf "AllocMayBeOutOfBounds _"
     | Any (AllocAssignedToGlobal v) -> Pretty.dprintf "AllocAssignedToGlobal %a" CilType.Varinfo.pretty  v
 end