RelationPriv (goblint.Goblint

module Q = Queries

module RelationComponents = RelationDomain.RelComponents

module type S = functor (RD : RelationDomain.RD) -> sig ... end

module Top : S

Top privatization, which doesn't track globals at all. This is unlike base's "none" privatization. which does track globals, but doesn't privatize them.

module type ProtectionBasedPrivParam = sig ... end

module ProtectionBasedPriv (Param : ProtectionBasedPrivParam) : S

Protection-Based Reading. Is unsound w.r.t. to locals escaping and becoming public.

module CommonPerMutex (RD : RelationDomain.RD) : sig ... end

module PerMutexMeetPrivBase (RD : RelationDomain.RD) : sig ... end

module PerMutexMeetPriv (Param : CommonPriv.AtomicParam) : S

Per-mutex meet.

module W : sig ... end

May written variables.

module type ClusterArg = functor (RD : RelationDomain.RD) -> sig ... end

module NoCluster : ClusterArg

No clustering.

module type ClusteringArg = sig ... end

module Clustering12 : ClusteringArg

All clusters of size 1 and 2.

module Clustering2 : ClusteringArg

All clusters of size 2.

module ClusteringPower : ClusteringArg

All subset clusters.

module ClusteringMax : ClusteringArg

One maximum cluster.

module DownwardClosedCluster
  (ClusteringArg : ClusteringArg)
  (RD : RelationDomain.RD) : 
  sig ... end

Clusters when clustering is downward-closed.

module ArbitraryCluster (ClusteringArg : ClusteringArg) : ClusterArg

Clusters when clustering is arbitrary (not necessarily downward-closed).

module PerMutexMeetPrivTID
  (Param : CommonPriv.AtomicParam)
  (Digest : CommonPriv.Digest)
  (Cluster : ClusterArg) : 
  S

Per-mutex meet with TIDs.

module TracingPriv (Priv : S) (RD : RelationDomain.RD) : sig ... end

val priv_module : (module S) Stdlib.Lazy.t

val get_priv : unit -> (module S)