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
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 : Cil.varinfo -> D.t
val morphstate : Cil.varinfo -> D.t -> D.t
val exitstate : Cil.varinfo -> D.t
val should_join : D.t -> D.t -> bool
val context : Cil.fundec -> D.t -> C.t
val call_descr : Cil.fundec -> C.t -> string
val sync : (D.t, G.t, C.t) Analyses.ctx -> [ `Normal | `Join | `Return ] -> D.t
val query : (D.t, G.t, C.t) Analyses.ctx -> 'a Queries.t -> 'a Queries.result
val assign : (D.t, G.t, C.t) Analyses.ctx -> Cil.lval -> Cil.exp -> D.t
val vdecl : (D.t, G.t, C.t) Analyses.ctx -> Cil.varinfo -> D.t
val branch : (D.t, G.t, C.t) Analyses.ctx -> Cil.exp -> bool -> D.t
val body : (D.t, G.t, C.t) Analyses.ctx -> Cil.fundec -> D.t
val return : (D.t, G.t, C.t) Analyses.ctx -> Cil.exp option -> Cil.fundec -> D.t
val intrpt : (D.t, G.t, C.t) Analyses.ctx -> D.t
val asm : (D.t, G.t, C.t) Analyses.ctx -> D.t
val skip : (D.t, G.t, C.t) Analyses.ctx -> D.t
val special : (D.t, G.t, C.t) Analyses.ctx -> Cil.lval option -> Cil.varinfo -> Cil.exp list -> D.t
val enter : (D.t, G.t, C.t) Analyses.ctx -> Cil.lval option -> Cil.fundec -> Cil.exp list -> (D.t * D.t) list
val combine : (D.t, G.t, C.t) Analyses.ctx -> Cil.lval option -> Cil.exp -> Cil.fundec -> Cil.exp list -> C.t -> D.t -> D.t
val threadenter : (D.t, G.t, C.t) Analyses.ctx -> Cil.lval option -> Cil.varinfo -> Cil.exp list -> D.t list

Returns initial state for created thread.

val threadspawn : (D.t, G.t, C.t) Analyses.ctx -> Cil.lval option -> Cil.varinfo -> Cil.exp list -> (D.t, G.t, C.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) Analyses.ctx -> Events.t -> (D.t, G.t, C.t) Analyses.ctx -> D.t