package goblint

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

Add path sensitivity to a analysis

Parameters

Signature

module D : Lattice.S with type t = HoareDomain.Set(Spec.D).t
module G = Spec.G
module C = Spec.C
module V = Spec.V

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

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