Merge pull request #1510 from goblint/mutexType-default

Enable `pthreadMutexType` analysis by default
goblint · Jun 25, 2024 · 52af9cd · 52af9cd
2 parents ad1ed06 + ecda3f7
commit 52af9cd
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -344,7 +344,7 @@
           "default": [
             "expRelation", "base", "threadid", "threadflag", "threadreturn",
             "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
-            "assert"
+            "assert", "pthreadMutexType"
           ]
         },
         "path_sens": {