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