package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

An analysis specification for didactic purposes. It only considers definite values of local variables. We do not pass information interprocedurally.

include Analyses.Spec
module D : Lattice.S
module G : Lattice.S
module C : Printable.S

Global constraint variables.

module P : DisjointDomain.Representative with type elt := D.t

Global constraint variables.

val name : unit -> string
type marshal

Auxiliary data (outside of solution domains) that needs to be marshaled and unmarshaled. This includes: * hashtables, * varinfos (create_var), * RichVarinfos.

val init : marshal option -> unit

Initialize using unmarshaled auxiliary data (if present).

val finalize : unit -> marshal

Finalize and return auxiliary data to be marshaled.

val startstate : GoblintCil.varinfo -> D.t
val morphstate : GoblintCil.varinfo -> D.t -> D.t
val exitstate : GoblintCil.varinfo -> D.t
val context : (D.t, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.fundec -> D.t -> C.t
val startcontext : unit -> C.t
val sync : (D.t, G.t, C.t, V.t) Analyses.ctx -> [ `Normal | `Join | `JoinCall | `Return ] -> D.t
val query : (D.t, G.t, C.t, V.t) Analyses.ctx -> 'a Queries.t -> 'a Queries.result

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

A transfer function used for declaring local variables. By default only for variable-length arrays (VLAs).

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

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

val body : (D.t, G.t, C.t, V.t) Analyses.ctx -> 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 return : (D.t, G.t, C.t, V.t) Analyses.ctx -> 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 asm : (D.t, G.t, C.t, V.t) Analyses.ctx -> D.t

A transfer function meant to handle inline assembler program points

val skip : (D.t, G.t, C.t, V.t) Analyses.ctx -> D.t

A transfer function which works as the identity function, i.e., it skips and does nothing. Used for empty loops.

val special : (D.t, G.t, C.t, V.t) Analyses.ctx -> 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 enter : (D.t, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> (D.t * D.t) list

For a function call "lval = f(args)" or "f(args)", enter returns a caller state, and the initial state of the callee. In enter, the caller state can usually be returned unchanged, as combine_env and combine_assign (below) will compute the caller state after the function call, given the return state of the callee

val combine_env : (D.t, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.exp -> GoblintCil.fundec -> GoblintCil.exp list -> C.t option -> D.t -> Queries.ask -> D.t

Combine environment (global variables, mutexes, etc) between local state (first component from enter) and function return.

This shouldn't yet assign to the lval.

val combine_assign : (D.t, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.exp -> GoblintCil.fundec -> GoblintCil.exp list -> C.t option -> D.t -> Queries.ask -> D.t

Combine return value assignment to local state (result from combine_env) and function return.

This should only assign to the lval.

val paths_as_set : (D.t, G.t, C.t, V.t) Analyses.ctx -> D.t list
val threadenter : (D.t, G.t, C.t, V.t) Analyses.ctx -> multiple:bool -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> D.t list

Returns initial state for created thread.

val threadspawn : (D.t, G.t, C.t, V.t) Analyses.ctx -> multiple:bool -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> (D.t, G.t, C.t, V.t) Analyses.ctx -> D.t

Updates the local state of the creator thread using initial state of created thread.

val event : (D.t, G.t, C.t, V.t) Analyses.ctx -> Events.t -> (D.t, G.t, C.t, V.t) Analyses.ctx -> D.t
module A : Analyses.MCPA
val access : (D.t, G.t, C.t, V.t) Analyses.ctx -> Queries.access -> A.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct