package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

dune-project
 Dependency

Authors

Maintainers

Sources

goblint-2.6.0.tbz
sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41
sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71

doc/goblint.solver/Goblint_solver/Generic/SoundBoxSolverImpl/index.html

Module Generic.SoundBoxSolverImplSource

Parameters

module H : Batteries.Hashtbl.S with type key = S.v

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 H.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 H.t -> unit
Sourceval stats_csv : unit BatIO.output option
Sourceval write_csv : string list -> unit BatIO.output -> unit
Sourceval print_stats : 'a -> unit
Sourceval h_find_default : 'a H.t -> H.key -> 'a -> 'a
Sourceval solveWithStart : (S.Dom.t H.t * S.Dom.t H.t) -> (H.key * S.Dom.t) list -> H.key list -> S.Dom.t H.t * S.Dom.t H.t
Sourceval solve : (H.key * S.Dom.t) list -> H.key list -> S.Dom.t H.t

the solve function