package goblint

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

Parameters

Signature

include sig ... end
module GU = Goblintutil
val stack_d : int Prelude.ref
val full_trace : bool
val start_c : int
val max_c : int Prelude.ref
val max_var : S.Var.t option Prelude.ref
val histo : int HM.t
val increase : S.Var.t -> unit
val start_event : unit -> unit
val stop_event : unit -> unit
val new_var_event : S.Var.t -> unit
val get_var_event : S.Var.t -> unit
val eval_rhs_event : S.Var.t -> unit
val update_var_event : S.Var.t -> S.Dom.t -> S.Dom.t -> unit
val print_solver_stats : (unit -> unit) Prelude.ref
val ncontexts : int Prelude.ref
val print_context_stats : 'a HM.t -> unit
val stats_csv : unit BatIO.output option
val write_csv : string list -> unit BatIO.output -> unit
val print_stats : 'a -> unit
module VS : sig ... end
type solver_data = {
  1. mutable st : (S.Var.t * S.Dom.t) list;
  2. mutable infl : VS.t HM.t;
  3. mutable sides : VS.t HM.t;
  4. mutable rho : S.Dom.t HM.t;
  5. mutable wpoint : unit HM.t;
  6. mutable stable : unit HM.t;
  7. mutable side_dep : VS.t HM.t;
    (*

    Dependencies of side-effected variables. Knowing these allows restarting them and re-triggering all side effects.

    *)
  8. mutable side_infl : VS.t HM.t;
    (*

    Influences to side-effected variables. Not normally in infl, but used for restarting them.

    *)
  9. mutable var_messages : Messages.Message.t HM.t;
    (*

    Messages from right-hand sides of variables. Used for incremental postsolving.

    *)
  10. mutable rho_write : S.Dom.t HM.t HM.t;
    (*

    Side effects from variables to write-only variables with values. Used for fast incremental restarting of write-only variables.

    *)
  11. mutable dep : VS.t HM.t;
    (*

    Dependencies of variables. Inverse of infl. Used for fast pre-reachable pruning in incremental postsolving.

    *)
}
type marshal = solver_data
val create_empty_data : unit -> solver_data
val print_data : solver_data -> string -> unit
val verify_data : solver_data -> unit
val exists_key : (HM.key -> bool) -> 'a HM.t -> bool
module P : sig ... end
module HPM : sig ... end
type phase =
  1. | Widen
  2. | Narrow
module CurrentVarS : sig ... end
module S = CurrentVarS.S
val solve : (S.Var.t -> S.Dom.t -> S.Dom.t -> S.Dom.t) -> (S.Var.t * S.Dom.t) list -> S.Var.t list -> S.Dom.t HM.t * solver_data
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