Goblint_lib.Td3Incremental/interactive terminating top-down solver, which supports space-efficiency and caching (td3).
Incremental terminating top down solver that optionally only keeps values at widening points and restores other values afterwards.
module type Hooks = sig ... endmodule Base
(Arg : Analyses.IncrSolverArg)
(S : Analyses.EqConstrSys)
(HM : Batteries.Hashtbl.S with type key = S.v)
(Hooks : Hooks with module S = S and module HM = HM) :
sig ... endmodule Basic : Analyses.GenericEqIncrSolverTD3 with no hooks.
module DepVals : Analyses.GenericEqIncrSolverTD3 with eval skipping using dep_vals.