diff --git a/src/analyses/mayLocksDigest.ml b/src/analyses/mayLocksDigest.ml new file mode 100644 index 0000000000..11b9a71094 --- /dev/null +++ b/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) diff --git a/tests/regression/46-apron2/58-lock-digest.c b/tests/regression/46-apron2/58-lock-digest.c index 6b1f909982..d1206df93b 100644 --- a/tests/regression/46-apron2/58-lock-digest.c +++ b/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 #include