CommonPerMutex (goblint.Goblint_lib.RelationPriv.CommonPerMutex)

Parameters

module RD : RelationDomain.RD

Signature

include module type of struct include CommonPriv.Protection end

val is_unprotected : 
  Queries.ask ->
  ?kind:Queries.ProtectionKind.t ->
  ?protection:Queries.Protection.t ->
  GoblintCil.varinfo ->
  bool

val is_unprotected_without : 
  Queries.ask ->
  ?kind:Queries.ProtectionKind.t ->
  ?protection:Queries.Protection.t ->
  CilType.Varinfo.t ->
  LockDomain.MustLock.t ->
  bool

val is_protected_by : 
  Queries.ask ->
  ?kind:Queries.ProtectionKind.t ->
  ?protection:Queries.Protection.t ->
  LockDomain.MustLock.t ->
  GoblintCil.varinfo ->
  bool

val protected_vars : 
  Queries.ask ->
  kind:Queries.ProtectionKind.t ->
  GoblintCil.varinfo list

module V = RD.V

val remove_globals_unprotected_after_unlock : 
  Queries.ask ->
  LockDomain.MustLock.t ->
  RD.t ->
  RD.t

val keep_only_protected_globals : 
  Queries.ask ->
  LockDomain.MustLock.t ->
  RD.t ->
  RD.t