Module RelationPriv.Top

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.

Parameters

Signature

module D : Lattice.S
module G : Lattice.S
module V : Printable.S
module P : DisjointDomain.Representative with type elt := D.t

Path-representative.

type relation_components_t := RelationDomain.RelComponents(RD)(D).t
val name : unit -> string
val startstate : unit -> D.t
val read_global : Queries.ask -> (V.t -> G.t) -> relation_components_t -> GoblintCil.varinfo -> GoblintCil.varinfo -> RD.t
val write_global : ?invariant:bool -> Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> GoblintCil.varinfo -> GoblintCil.varinfo -> relation_components_t
val sync : Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [ `Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread ] -> relation_components_t
val enter_multithreaded : Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> relation_components_t
val thread_join : ?force:bool -> Queries.ask -> (V.t -> G.t) -> GoblintCil.Cil.exp -> relation_components_t -> relation_components_t
val thread_return : Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> relation_components_t -> relation_components_t
val iter_sys_vars : (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit

Queries.IterSysVars for apron.

val invariant_vars : Queries.ask -> (V.t -> G.t) -> relation_components_t -> GoblintCil.varinfo list

Returns global variables which are privatized.

val init : unit -> unit
val finalize : unit -> unit