Deduplicate Svcomp.is_error_function

goblint · Oct 31, 2023 · bb163a5 · bb163a5
1 parent 5093b5d
commit bb163a5
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 12 deletions.
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
@@ -324,10 +324,8 @@ class loopUnrollingCallVisitor = object
           raise Found;
         | _ ->
           if List.mem "specification" @@ get_string_list "ana.autotune.activated" && get_string "ana.specification" <> "" then (
-            List.iter (function
-                | SvcompSpec.UnreachCall s -> if info.vname = s then raise Found
-                | _ -> ()
-              ) (SvcompSpec.of_option ())
+            if Svcomp.is_error_function' info (SvcompSpec.of_option ()) then
+              raise Found
           );
           DoChildren
       )

diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
@@ -16,25 +16,24 @@ end
 let task: (module Task) option ref = ref None
 
 
-let is_error_function f =
+let is_error_function' f spec =
   let module Task = (val (Option.get !task)) in
   List.exists (function
       | Specification.UnreachCall f_spec -> f.vname = f_spec
       | _ -> false
-    ) Task.specification
+    ) spec
+
+let is_error_function f =
+  let module Task = (val (Option.get !task)) in
+  is_error_function' f Task.specification
 
 (* TODO: unused, but should be used? *)
 let is_special_function f =
   let loc = f.vdecl in
   let is_svcomp = String.ends_with loc.file "sv-comp.c" in (* only includes/sv-comp.c functions, not __VERIFIER_assert in benchmark *)
   let is_verifier = match f.vname with
     | fname when String.starts_with fname "__VERIFIER" -> true
-    | fname ->
-      let module Task = (val (Option.get !task)) in
-      List.exists (function
-          | Specification.UnreachCall f_spec -> fname = f_spec
-          | _ -> false
-        ) Task.specification
+    | fname -> is_error_function f
   in
   is_svcomp && is_verifier