Module Goblint_lib.RelationPriv

Relational thread-modular value analyses for RelationAnalysis, i.e. ApronAnalysis and AffineEqualityAnalysis.

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

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

Per-mutex meet.

module W : sig ... end

May written variables.

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

No clustering.

module type ClusteringArg = sig ... end

All clusters of size 1 and 2.

All clusters of size 2.

All subset clusters.

One maximum cluster.

Clusters when clustering is downward-closed.

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

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)