package goblint

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

Module Td3.BaseSource

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
Sourceval stack_d : int ref
Sourceval full_trace : bool
Sourceval start_c : int
Sourceval max_c : int ref
Sourceval max_var : S.Var.t option ref
Sourceval histo : int HM.t
Sourceval increase : S.Var.t -> unit
Sourceval start_event : unit -> unit
Sourceval stop_event : unit -> unit
Sourceval new_var_event : S.Var.t -> unit
Sourceval get_var_event : S.Var.t -> unit
Sourceval eval_rhs_event : S.Var.t -> unit
Sourceval update_var_event : S.Var.t -> S.Dom.t -> S.Dom.t -> unit
Sourceval print_solver_stats : (unit -> unit) ref
Sourceval ncontexts : int ref
Sourceval print_context_stats : 'a HM.t -> unit
Sourceval stats_csv : unit BatIO.output option
Sourceval write_csv : string list -> unit BatIO.output -> unit
Sourceval print_stats : 'a -> unit
Sourcemodule VS : sig ... end
Sourceval exists_key : (HM.key -> bool) -> 'a HM.t -> bool
Sourcetype 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.

    *)
}
Sourcetype marshal = solver_data
Sourceval create_empty_data : unit -> solver_data
Sourceval print_data : solver_data -> unit
Sourceval print_data_verbose : solver_data -> string -> unit
Sourceval verify_data : solver_data -> unit
Sourceval copy_marshal : marshal -> marshal
Sourceval relift_marshal : marshal -> marshal
Sourcetype phase =
  1. | Widen
  2. | Narrow
Sourcemodule CurrentVarS : sig ... end
Sourceval 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 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