diff --git a/conf/svcomp.json b/conf/svcomp.json index 913d43784b..df624e4b83 100644 --- 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,7 +60,8 @@ "ldv_xmalloc", "ldv_xzalloc", - "ldv_calloc" + "ldv_calloc", + "ldv_kzalloc" ] }, "base": { @@ -60,6 +69,10 @@ "domain": "partitioned" } }, + "race": { + "free": false, + "call": false + }, "autotune": { "enabled": true, "activated": [ 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/maingoblint.ml b/src/maingoblint.ml index 7808cbcd3f..036f4b3fcc 100644 --- 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 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.",