sig
type state
type eval_env
val env_current_state :
Abstract_domain.Logic.eval_env ->
Abstract_domain.Logic.state Eval.or_bottom
val env_annot :
pre:Abstract_domain.Logic.state ->
here:Abstract_domain.Logic.state ->
unit -> Abstract_domain.Logic.eval_env
val env_pre_f :
pre:Abstract_domain.Logic.state -> unit -> Abstract_domain.Logic.eval_env
val env_post_f :
pre:Abstract_domain.Logic.state ->
post:Abstract_domain.Logic.state ->
result:Cil_types.varinfo option -> unit -> Abstract_domain.Logic.eval_env
val eval_predicate :
Abstract_domain.Logic.eval_env -> Cil_types.predicate -> Alarmset.status
val reduce_by_predicate :
Abstract_domain.Logic.eval_env ->
bool -> Cil_types.predicate -> Abstract_domain.Logic.eval_env
end