diff --git a/conf/svcomp.json b/conf/svcomp.json index 73f99500b9..293898690c 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -32,6 +32,15 @@ "thread", "threadJoins" ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], "context": { "widen": false }, @@ -52,7 +61,8 @@ "ldv_xmalloc", "ldv_xzalloc", - "ldv_calloc" + "ldv_calloc", + "ldv_kzalloc" ] }, "base": { @@ -60,6 +70,10 @@ "domain": "partitioned" } }, + "race": { + "free": false, + "call": false + }, "autotune": { "enabled": true, "activated": [ diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 4e282b19a4..0b5b9d70a6 100644 --- a/src/common/util/options.schema.json +++ b/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.", diff --git a/src/domains/access.ml b/src/domains/access.ml index 3ba7aaee74..baa9d34220 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; _} = | 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. *) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 1512e63b47..98f73a12bb 100644 --- a/src/maingoblint.ml +++ b/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 =