Merge branch 'svcomp24-conf' into pldi-bench

goblint · Oct 9, 2023 · e4bf5ac · e4bf5ac
2 parents 0af8ba7 + 94307d0
commit e4bf5ac
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 1 deletion.
diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -32,6 +32,14 @@
       "thread",
       "threadJoins"
     ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "threadid"
+    ],
     "context": {
       "widen": false
     },
@@ -52,14 +60,19 @@
 
         "ldv_xmalloc",
         "ldv_xzalloc",
-        "ldv_calloc"
+        "ldv_calloc",
+        "ldv_kzalloc"
       ]
     },
     "base": {
       "arrays": {
         "domain": "partitioned"
       }
     },
+    "race": {
+      "free": false,
+      "call": false
+    },
     "autotune": {
       "enabled": true,
       "activated": [

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/maingoblint.ml b/src/maingoblint.ml
@@ -252,6 +252,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 =

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.",