Module BaseInvariant.Make

Parameters

module Eval : Eval

Signature

val is_some_bot : VD.t -> bool
val apply_invariant : old_val:VD.t -> new_val:VD.t -> VD.t
val refine_lv_fallback : (Eval.D.t, Eval.G.t, 'a, Eval.V.t) Analyses.man -> Eval.D.t -> GoblintCil.lval -> VD.t -> bool -> Eval.D.t
val refine_lv : (Eval.D.t, Eval.G.t, 'a, Eval.V.t) Analyses.man -> Eval.D.t -> 'b -> GoblintCil.lval -> VD.t -> (unit -> 'b -> GoblintCil.Pretty.doc) -> GoblintCil.exp -> Eval.D.t
val invariant_fallback : (Eval.D.t, Eval.G.t, 'a, Eval.V.t) Analyses.man -> Eval.D.t -> GoblintCil.exp -> bool -> Eval.D.t
val invariant : (Eval.D.t, Eval.G.t, 'a, Eval.V.t) Analyses.man -> Eval.D.t -> GoblintCil.exp -> bool -> Eval.D.t