Merge branch 'master' into svcomp24-dev

goblint · Nov 24, 2023 · c2e9465 · c2e9465
2 parents e0a0692 + 3540ae2
commit c2e9465
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 1 deletion.
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -99,7 +99,9 @@ let rec setCongruenceRecursive fd depth neigbourFunction =
     FunctionSet.iter
       (fun vinfo ->
          print_endline ("    " ^ vinfo.vname);
-         setCongruenceRecursive (Cilfacade.find_varinfo_fundec vinfo) (depth -1) neigbourFunction
+         match Cilfacade.find_varinfo_fundec vinfo with
+         | fd -> setCongruenceRecursive fd (depth -1) neigbourFunction
+         | exception Not_found -> () (* Happens for __goblint_bounded *)
       )
       (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*)
          (fun x -> not (isExtern x.vstorage || BatString.starts_with x.vname "__builtin"))

diff --git a/tests/regression/78-termination/51-modulo.c b/tests/regression/78-termination/51-modulo.c
@@ -0,0 +1,14 @@
+// SKIP TERM PARAM: --enable ana.autotune.enabled --enable ana.sv-comp.functions --enable ana.sv-comp.enabled  --set ana.autotune.activated "['congruence']" --set ana.specification "CHECK( init(main()), LTL(F end) )"
+
+// This task previously crashed due to the autotuner
+int main() {
+	int a;
+    int odd, count = 0;
+    while(a > 1) {
+      odd = a % 2;
+      if(!odd) a = a / 2;
+      else a = a - 1;
+      count++;
+    }
+    return count;
+}