package goblint

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

Limits the number of widenings per node.

Parameters

module S : Analyses.Spec

Signature

include module type of S with module D := S.D and type marshal = S.marshal
module G : Lattice.S
module C : Printable.S
type marshal = S.marshal

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

val finalize : unit -> marshal

Finalize and return auxiliary data to be marshaled.

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

Returns initial state for created thread.

val threadspawn : (S.D.t, G.t, C.t) Analyses.ctx -> Cil.lval option -> Cil.varinfo -> Cil.exp list -> (S.D.t, G.t, C.t) Analyses.ctx -> S.D.t

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

val name : unit -> string
val limit : int Prelude.ref
val init : S.marshal option -> unit
module H = MyCFG.NodeH
val h : int H.t
val incr : H.key -> unit
module D : sig ... end
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