Parameter FromSimplifiedSpec.S

Set of globals.

module G : Lattice.S

Domain for globals.

module D : Lattice.S

Domain for globals.

module C : Printable.S

Context information.

val name : string

Name of the analysis.

val startstate : D.t

Initial local state for main.

val startcontext : C.t

Initial local state for main.

Initial context for main.

val assign : (G.t, C.t, V.t) SimplifiedAnalysis.man -> D.t -> GoblintCil.lval -> GoblintCil.exp -> D.t

A transfer function which handles the assignment of a rval to a lval, i.e., it handles program points of the form "lval = rval;"

val branch : (G.t, C.t, V.t) SimplifiedAnalysis.man -> D.t -> GoblintCil.exp -> bool -> D.t

A transfer function which handles conditional branching yielding the truth value passed as a boolean argument

val return : (G.t, C.t, V.t) SimplifiedAnalysis.man -> D.t -> GoblintCil.exp option -> GoblintCil.fundec -> D.t

A transfer function which handles the return statement, i.e., "return exp" or "return" in the passed function (fundec)

val body : (G.t, C.t, V.t) SimplifiedAnalysis.man -> D.t -> GoblintCil.fundec -> D.t

A transfer function which handles going from the start node of a function (fundec) into its function body. Meant to handle, e.g., initialization of local variables

val enter : (G.t, C.t, V.t) SimplifiedAnalysis.man -> D.t -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> D.t

For a function call "lval = f(args)" or "f(args)", enter returns the initial state of the callee.

val combine : (G.t, C.t, V.t) SimplifiedAnalysis.man -> D.t -> D.t -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> D.t

Combines the states before and after the call.

val special : (G.t, C.t, V.t) SimplifiedAnalysis.man -> D.t -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> D.t

A transfer function which, for a call to a special function f "lval = f(args)" or "f(args)", computes the caller state after the function call

val context : (G.t, C.t, V.t) SimplifiedAnalysis.man -> (D.t * C.t) -> GoblintCil.fundec -> D.t -> C.t

Compute the context for a function call, given the local state and context at the caller, the called function and the local state inside the callee

val threadenter : (G.t, C.t, V.t) SimplifiedAnalysis.man -> D.t -> GoblintCil.fundec -> GoblintCil.exp list -> D.t

Compute the start state of a new thread starting with the function given by fundec