package goblint

  1. Overview
  2. Docs
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.

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 should_join : D.t -> D.t -> bool
val context : GoblintCil.fundec -> D.t -> C.t
val sync : (D.t, G.t, C.t, V.t) Analyses.ctx -> [ `Normal | `Join | `Return ] -> D.t
val query : (D.t, G.t, C.t, V.t) Analyses.ctx -> 'a Queries.t -> 'a Queries.result
val branch : (D.t, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.exp -> bool -> D.t
val return : (D.t, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.exp option -> GoblintCil.fundec -> D.t
val asm : (D.t, G.t, C.t, V.t) Analyses.ctx -> D.t
val skip : (D.t, G.t, C.t, V.t) Analyses.ctx -> D.t
val special : (D.t, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> D.t
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
val combine : (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 -> D.t
val threadenter : (D.t, G.t, C.t, V.t) Analyses.ctx -> 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 -> 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.