diff --git a/conf/examples/medium-program.json b/conf/examples/medium-program.json index 2c1e7c7346..5afc1aa2f8 100644 --- a/conf/examples/medium-program.json +++ b/conf/examples/medium-program.json @@ -9,6 +9,7 @@ "base", "threadid", "threadflag", + "threadreturn", "mallocWrapper", "mutexEvents", "mutex", @@ -18,6 +19,7 @@ "expRelation", "mhp", "assert", + "pthreadMutexType", "var_eq", "symb_locks", "region", diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json index 2197335eaf..074d448a85 100644 --- a/conf/examples/very-precise.json +++ b/conf/examples/very-precise.json @@ -22,6 +22,7 @@ "base", "threadid", "threadflag", + "threadreturn", "mallocWrapper", "mutexEvents", "mutex", @@ -31,6 +32,7 @@ "expRelation", "mhp", "assert", + "pthreadMutexType", "var_eq", "symb_locks", "region", diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml index 441f2e9953..4a993bbd7d 100644 --- a/src/analyses/mutexTypeAnalysis.ml +++ b/src/analyses/mutexTypeAnalysis.ml @@ -12,16 +12,17 @@ struct let name () = "pthreadMutexType" - (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *) - module O = Offset.Unit - - module V = struct - include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *) + module V = + struct + (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *) + include Mval.Unit let is_write_only _ = false end module G = MAttr + module O = Offset.Unit + (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = match lval with diff --git a/src/autoTune.ml b/src/autoTune.ml index 434b4fb0b2..8ec77739e7 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -186,7 +186,7 @@ let enableAnalyses anas = (*escape is also still enabled, because otherwise we get a warning*) (*does not consider dynamic calls!*) -let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"] +let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"] let reduceThreadAnalyses () = let isThreadCreate = function | LibraryDesc.ThreadCreate _ -> true diff --git a/src/config/options.schema.json b/src/config/options.schema.json index acf85abed9..d259a6f418 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -344,7 +344,7 @@ "default": [ "expRelation", "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", - "assert" + "assert", "pthreadMutexType" ] }, "path_sens": {