package goblint

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

Analysis specification and constraint system signatures.

module M = Messages
type fundecs = GoblintCil.fundec list * GoblintCil.fundec list * GoblintCil.fundec list

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

module Var : sig ... end
module VarF (LD : Printable.S) : sig ... end
module type SpecSysVar = sig ... end
module GVarF (V : SpecSysVar) : sig ... end
module GVarFC (V : SpecSysVar) (C : Printable.S) : sig ... end
module GVarG (G : Lattice.S) (C : Printable.S) : sig ... end
exception Deadcode
module Dom (LD : Lattice.S) : sig ... end

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

type ('d, 'g, 'c, 'v) 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 : unit -> ControlSpecC.t;
    (*

    top-level Control Spec context, raises Ctx_failure if missing

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

    current Spec context, raises Ctx_failure if missing

    *)
  7. edge : MyCFG.edge;
  8. local : 'd;
  9. global : 'v -> 'g;
  10. spawn : ?multiple:bool -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> unit;
  11. split : 'd -> Events.t list -> unit;
  12. sideg : 'v -> 'g -> 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, 'd) ctx -> Queries.ask

Convert ctx to Queries.ask.

module type Spec = sig ... end
module type Spec2Spec = functor (S : Spec) -> Spec
module type MCPA = sig ... end
module type MCPSpec = sig ... end
type increment_data = {
  1. server : bool;
  2. solver_data : Stdlib.Obj.t;
  3. changes : CompareCIL.change_info;
  4. restarting : VarQuery.t list;
}
module StdV : sig ... end
module UnitV : sig ... end
module VarinfoV : sig ... end
module EmptyV : sig ... end
module UnitA : sig ... end
module UnitP : sig ... end
module IdentityP (D : Lattice.S) : sig ... end
module DefaultSpec : sig ... end

Relatively safe default implementations of some boring Spec functions.

module IdentitySpec : sig ... end
module IdentityUnitContextsSpec : sig ... end
module ValueContexts (D : Lattice.S) : sig ... end
module type SpecSys = sig ... end
module type SpecSysSol = 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