package goblint

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

Signatures for analyzers, analysis specifications, and result output.

module GU = Goblintutil
module M = Messages
type fundecs = Cil.fundec list * Cil.fundec list * Cil.fundec list

Analysis starts from lists of functions: start functions, exit functions, and * other functions.

module type VarType = sig ... end
module Var : sig ... end
module VarF (LD : Printable.S) : sig ... end
exception Deadcode
module Dom (LD : Lattice.S) : sig ... end

Dom (D) produces D lifted where bottom means dead-code

module ResultNode : Printable.S with type t = MyCFG.node
module type ResultConf = sig ... end
module Result (Range : Printable.S) (C : ResultConf) : sig ... end
type ('d, 'g, 'c) ctx = {
  1. ask : 'a. 'a Queries.t -> 'a Queries.result;
  2. emit : Events.t -> unit;
  3. node : MyCFG.node;
  4. prev_node : MyCFG.node;
  5. control_context : Obj.t;
    (*

    (Control.get_spec ()) context, represented type: unit -> (Control.get_spec ()).C.t

    *)
  6. context : unit -> 'c;
    (*

    current Spec context

    *)
  7. edge : MyCFG.edge;
  8. local : 'd;
  9. global : Cil.varinfo -> 'g;
  10. presub : (string * Obj.t) list;
  11. postsub : (string * Obj.t) list;
  12. spawn : Cil.lval option -> Cil.varinfo -> Cil.exp list -> unit;
  13. split : 'd -> Events.t list -> unit;
  14. sideg : Cil.varinfo -> 'g -> unit;
  15. assign : ?name:string -> Cil.lval -> Cil.exp -> unit;
}
exception Ctx_failure of string

Failure from ctx, e.g. global initializer

val ctx_failwith : string -> 'a
val ask_of_ctx : ('a, 'b, 'c) ctx -> Queries.ask

Convert ctx to Queries.ask.

val swap_st : ('a, 'b, 'c) ctx -> 'a -> ('a, 'b, 'c) ctx
val set_st_gl : ('a, 'b, 'c) ctx -> 'd -> (Cil.varinfo -> 'e) -> ((Cil.lval option -> Cil.varinfo -> Cil.exp list -> unit) -> Cil.lval option -> Cil.varinfo -> Cil.exp list -> unit) -> ((Cil.varinfo -> 'b -> unit) -> Cil.varinfo -> 'e -> unit) -> (('a -> Events.t list -> unit) -> 'd -> Events.t list -> unit) -> ('d, 'e, 'c) ctx
module type Spec = sig ... end
module type MCPSpec = sig ... end
type analyzed_data = {
  1. cil_file : Cil.file;
  2. solver_data : Obj.t;
}
type increment_data = {
  1. old_data : analyzed_data option;
  2. new_file : Cil.file;
  3. changes : CompareCIL.change_info;
}
val empty_increment_data : Cil.file -> increment_data
module type MonSystem = sig ... end

A side-effecting system.

module type EqConstrSys = MonSystem with type 'a m := 'a option

Any system of side-effecting equations over lattices.

module type GlobConstrSys = sig ... end

A side-effecting system with globals.

module type GenericEqBoxIncrSolverBase = functor (S : EqConstrSys) -> functor (H : Prelude.Hashtbl.S with type key = S.v) -> sig ... end

A solver is something that can translate a system into a solution (hash-table). Incremental solver has data to be marshaled.

module type IncrSolverArg = sig ... end

(Incremental) solver argument, indicating which postsolving should be performed by the solver.

An incremental solver takes the argument about postsolving.

module type GenericEqBoxSolver = functor (S : EqConstrSys) -> functor (H : Prelude.Hashtbl.S with type key = S.v) -> sig ... end

A solver is something that can translate a system into a solution (hash-table)

module type GenericGlobSolver = functor (S : GlobConstrSys) -> functor (LH : Prelude.Hashtbl.S with type key = S.LVar.t) -> functor (GH : Prelude.Hashtbl.S with type key = S.GVar.t) -> sig ... end

A solver is something that can translate a system into a solution (hash-table)

module ResultType2 (S : Spec) : sig ... end
module DefaultSpec : sig ... end

Relatively safe default implementations of some boring Spec functions.

module IdentitySpec : 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