From 94307d03c47d63621ade9b833c0be35bb23bee89 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 Oct 2023 17:27:55 +0300
Subject: [PATCH] Add option ana.race.call

---
 conf/svcomp.json             | 3 ++-
 src/domains/access.ml        | 2 ++
 src/util/options.schema.json | 6 ++++++
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/conf/svcomp.json b/conf/svcomp.json
index f51c7a52ee..df624e4b83 100644
--- 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
index 8907ccbc32..f243b85bda 100644
--- 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
index 1b9c7d3fd5..33de069b38 100644
--- 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.",