package goblint

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

Parameters

module HM : Batteries.Hashtbl.S with type key = S.v
module Hooks : Hooks with module S = S and module HM = HM

Signature

include sig ... end
val stack_d : int Stdlib.ref
val full_trace : bool
val start_c : int
val max_c : int Stdlib.ref
val max_var : S.Var.t option Stdlib.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) Stdlib.ref
val ncontexts : int Stdlib.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
val exists_key : (HM.key -> bool) -> 'a HM.t -> bool
type solver_data = {
  1. st : (S.Var.t * S.Dom.t) list;
  2. infl : VS.t HM.t;
  3. sides : VS.t HM.t;
  4. rho : S.Dom.t HM.t;
  5. wpoint : unit HM.t;
  6. stable : unit HM.t;
  7. side_dep : VS.t HM.t;
    (*

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

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

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

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

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

    *)
  10. 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. 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 -> unit
val print_data_verbose : solver_data -> string -> unit
val verify_data : solver_data -> unit
val copy_marshal : marshal -> marshal
val relift_marshal : marshal -> marshal
type phase =
  1. | Widen
  2. | Narrow
val pp_phase : Ppx_deriving_runtime.Format.formatter -> phase -> Ppx_deriving_runtime.unit
module CurrentVarS : sig ... end
module S = CurrentVarS.S
val solve : (S.Var.t * S.Dom.t) list -> HM.key list -> solver_data option -> 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 Blog 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