Module C2poAnalysis.Spec

include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

include module type of struct include Analyses.IdentitySpec end
include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

module G = Lattice.Unit
module V = Analyses.EmptyV
module P = Analyses.UnitP
type marshal = unit
val init : 'a -> unit
val finalize : unit -> unit
val vdecl : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'f
val asm : ('a, 'b, 'c, 'd) Analyses.man -> 'e
val skip : ('a, 'b, 'c, 'd) Analyses.man -> 'e
val event : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'f -> 'g
val morphstate : 'a -> 'b -> 'c
val sync : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'f
val context : 'a -> 'b -> 'c -> 'd
val paths_as_set : ('a, 'b, 'c, 'd) Analyses.man -> 'e list
module A = Analyses.UnitA
val access : 'a -> 'b -> unit
module D = C2poDomain.D
module C = D
val name : unit -> string
val startcontext : unit -> [> `Lifted of CongruenceClosure.t ]
val reachable_from_args : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.exp list -> GoblintCil.varinfo list

Find reachable variables in a function

val eval_guard : Queries.ask -> CongruenceClosure.t -> GoblintCil.Cil.exp -> GoblintCil.Cil.ikind -> [> `Lifted of ValueDomainQueries.ID.I.t | `Top ]
val conj_to_invariant : 'a -> Goblint_lib__UnionFind.prop list -> [ `Bot | `Lifted of Invariant.ExpLat.t | `Top ]

Convert a conjunction to an invariant.

val query : ([< `Bot | `Lifted of CongruenceClosure.t ], 'b, 'c, 'd) Analyses.man -> 'a Queries.t -> 'a0 Queries.result
val assign_term : CongruenceClosure.t -> Queries.ask -> UnionFind.T.t -> (UnionFind.T.t option * Z.t option) -> GoblintCil.Cil.typ -> CongruenceClosure.t

Assign the right hand side rhs (that is already converted to a C-2PO term) to the term `lterm`.

val assign_lval : CongruenceClosure.t -> Queries.ask -> GoblintCil.lval -> (UnionFind.T.t option * Z.t option) -> CongruenceClosure.t

Assign Cil Lval to a right hand side that is already converted to C-2PO terms.

val assign : ([< `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man -> GoblintCil.lval -> GoblintCil.exp -> [> `Bot | `Lifted of CongruenceClosure.t ]
val branch : ([< `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man -> GoblintCil.Cil.exp -> bool -> [> `Bot | `Lifted of CongruenceClosure.t ]
val body : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'f
val assign_return : Queries.ask -> CongruenceClosure.t -> CongruenceClosure.term -> GoblintCil.exp -> CongruenceClosure.t
val return : ([ `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man -> GoblintCil.exp option -> 'd -> [ `Bot | `Lifted of CongruenceClosure.t ]
val special : ([ `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man -> GoblintCil.lval option -> GoblintCil.Cil.varinfo -> LibraryDesc.Cil.Cil.exp list -> [ `Bot | `Lifted of CongruenceClosure.t ]

var_opt is the variable we assign to. It has type lval. v=malloc.

val enter : ([< `Bot | `Lifted of CongruenceClosure.t & CongruenceClosure.t Bot ] as 'a, 'b, 'c, 'd) Analyses.man -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> ('e * [> `Bot | `Lifted of CongruenceClosure.t ]) list

First all local variables of the function are duplicated, then we remember the value of each local variable at the beginning of the function by using the analysis startState. This way we can infer the relations between the local variables of the caller and the pointers that were modified by the function.

val remove_out_of_scope_vars : CongruenceClosure.data -> GoblintCil.fundec -> CongruenceClosure.data
val combine_env : ([< `Bot | `Lifted of CongruenceClosure.t & CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man -> GoblintCil.lval option -> 'd -> GoblintCil.fundec -> GoblintCil.exp list -> 'e -> [< `Bot | `Lifted of CongruenceClosure.t & CongruenceClosure.t ] -> Queries.ask -> [> `Bot | `Lifted of CongruenceClosure.t ]
val combine_assign : ([< `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man -> GoblintCil.lval option -> 'd -> GoblintCil.fundec -> GoblintCil.exp list -> 'e -> [< `Bot | `Lifted of CongruenceClosure.t ] -> Queries.ask -> [> `Bot | `Lifted of CongruenceClosure.t ]
val startstate : 'a -> [> `Lifted of CongruenceClosure.t ]
val threadenter : 'a -> multiple:'b -> 'c -> 'd -> 'e -> [> `Lifted of CongruenceClosure.t ] list
val threadspawn : 'a -> multiple:'b -> 'c -> 'd -> 'e -> 'f -> [> `Lifted of CongruenceClosure.t ]
val exitstate : 'a -> [> `Lifted of CongruenceClosure.t ]