Improve SV-COMP conf for no-data-race

conf/svcomp.json

@@ -32,6 +32,15 @@
       "thread",
       "threadJoins"
     ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
     "context": {
       "widen": false
     },
@@ -52,14 +61,19 @@
 
         "ldv_xmalloc",
         "ldv_xzalloc",
-        "ldv_calloc"
+        "ldv_calloc",
+        "ldv_kzalloc"
       ]
     },
     "base": {
       "arrays": {
         "domain": "partitioned"
       }
     },
+    "race": {
+      "free": false,
+      "call": false
+    },
     "autotune": {
       "enabled": true,
       "activated": [

src/common/util/options.schema.json

@@ -1008,6 +1008,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.",

src/domains/access.ml

@@ -444,6 +444,8 @@ let may_race A.{kind; acc; _} A.{kind=kind2; acc=acc2; _} =
   | Read, Read -> false (* two read/read accesses do not race *)
   | Free, _
   | _, Free when not (get_bool "ana.race.free") -> false
+  | Call, _
+  | _, Call when not (get_bool "ana.race.call") -> false
   | _, _ -> MCPAccess.A.may_race acc acc2 (* analysis-specific information excludes race *)
 
 (** Access sets for race detection and warnings. *)

src/maingoblint.ml

@@ -256,6 +256,15 @@ let preprocess_files () =
   (* Preprocessor flags *)
   let cppflags = ref (get_string_list "pre.cppflags") in
 
+  if get_bool "ana.sv-comp.enabled" then (
+    let architecture_flag = match get_string "exp.architecture" with
+      | "32bit" -> "-m32"
+      | "64bit" -> "-m64"
+      | _ -> assert false
+    in
+    cppflags := architecture_flag :: !cppflags
+  );
+
   (* the base include directory *)
   (* TODO: any better way? dune executable promotion doesn't add _build sites *)
   let source_lib_dirs =