Add option ana.race.call

goblint · Oct 5, 2023 · 94307d0 · 94307d0
1 parent 11164fd
commit 94307d0
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 1 deletion.
diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -70,7 +70,8 @@
       }
     },
     "race": {
-      "free": false
+      "free": false,
+      "call": false
     },
     "autotune": {
       "enabled": true,

diff --git a/src/domains/access.ml b/src/domains/access.ml
@@ -444,6 +444,8 @@ let may_race A.{kind; acc; _} A.{kind=kind2; acc=acc2; _} =
     false (* two read/read accesses do not race *)
   else if not (get_bool "ana.race.free") && (kind = Free || kind2 = Free) then
     false
+  else if not (get_bool "ana.race.call") && (kind = Call || kind2 = Call) then
+    false
   else if not (MCPAccess.A.may_race acc acc2) then
     false (* analysis-specific information excludes race *)
   else

diff --git a/src/util/options.schema.json b/src/util/options.schema.json
@@ -1002,6 +1002,12 @@
               "type": "boolean",
               "default": true
             },
+            "call": {
+              "title": "ana.race.call",
+              "description": "Report races for thread-unsafe function calls.",
+              "type": "boolean",
+              "default": true
+            },
             "direct-arithmetic": {
               "title": "ana.race.direct-arithmetic",
               "description": "Collect and distribute direct (i.e. not in a field) accesses to arithmetic types.",