MainFunctor.Invariantval is_some_bot : ValueDomain.Compound.t -> boolval apply_invariant :
old_val:ValueDomain.Compound.t ->
new_val:ValueDomain.Compound.t ->
ValueDomain.Compound.tval refine_lv_fallback :
(InvariantEval.D.t, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
InvariantEval.D.t ->
GoblintCil.lval ->
ValueDomain.Compound.t ->
bool ->
InvariantEval.D.tval refine_lv :
(InvariantEval.D.t, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
InvariantEval.D.t ->
'b ->
GoblintCil.lval ->
ValueDomain.Compound.t ->
(unit -> 'b -> GoblintCil.Pretty.doc) ->
GoblintCil.exp ->
InvariantEval.D.tval invariant_fallback :
(InvariantEval.D.t, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
InvariantEval.D.t ->
GoblintCil.exp ->
bool ->
InvariantEval.D.tval invariant :
(InvariantEval.D.t, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
InvariantEval.D.t ->
GoblintCil.exp ->
bool ->
InvariantEval.D.t