package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.5.0.tbz
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/src/goblint.solver/selector.ml.html
Source file selector.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
(** Solver, which delegates at runtime to the configured solver. *) open Batteries open ConstrSys open GobConfig (* Registered solvers. *) let solvers = ref [] (** Register your solvers here!!! *) let add_solver x = solvers := x::!solvers (** Dynamically choose the solver. *) let choose_solver solver = try List.assoc solver !solvers with Not_found -> raise @@ ConfigError ("Solver '"^solver^"' not found. Abort!") (** The solver that actually uses the implementation based of [GobConfig.get_string "solver"]. *) module Make = functor (Arg: IncrSolverArg) -> functor (S:EqConstrSys) -> functor (VH:Hashtbl.S with type key = S.v) -> struct type marshal = Obj.t (* cannot use Sol.marshal because cannot unpack first-class module in applicative functor *) let copy_marshal (marshal: marshal) = let module Sol = (val choose_solver (get_string "solver") : GenericEqIncrSolver) in let module F = Sol (Arg) (S) (VH) in Obj.repr (F.copy_marshal (Obj.obj marshal)) let relift_marshal (marshal: marshal) = let module Sol = (val choose_solver (get_string "solver") : GenericEqIncrSolver) in let module F = Sol (Arg) (S) (VH) in Obj.repr (F.relift_marshal (Obj.obj marshal)) let solve xs vs (old_data: marshal option) = let module Sol = (val choose_solver (get_string "solver") : GenericEqIncrSolver) in let module F = Sol (Arg) (S) (VH) in let (vh, marshal) = F.solve xs vs (Option.map Obj.obj old_data) in (vh, Obj.repr marshal) end let _ = let module T1 : GenericEqIncrSolver = Make in ()
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>