Merge pull request #1271 from goblint/not_found_autotuner_termination

Fix `Not_found` exception in autotuner with congruences and termination.

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"))

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;
+}