Add maylocksdigest analysis

src/analyses/mayLocksDigest.ml

@@ -0,0 +1,30 @@
+(** May lockset digest analysis ([maylocksdigest]). *)
+
+open Analyses
+open GoblintCil
+module LF = LibraryFunctions
+
+module Arg:LocksetAnalysis.MayArg =
+struct
+  module D = LockDomain.MayLocksetNoRW
+  module P = IdentityP (D)
+  module G = DefaultSpec.G
+  module V = DefaultSpec.V
+
+  let add ctx (l,r) =
+    D.add l ctx.local
+
+  let remove ctx l =
+    ctx.local
+end
+
+module Spec =
+struct
+  include LocksetAnalysis.MakeMay (Arg)
+  let name () = "maylocksdigest"
+
+  let threadenter ctx ~multiple lval f args = [ctx.local]
+end
+
+let _ =
+  MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec)

tests/regression/46-apron2/58-lock-digest.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet
+// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.activated[+] maylocksdigest --set ana.path_sens[+] maylocksdigest
 #include <pthread.h>
 #include <goblint.h>