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 Cil_types.named -> Alarmset.status
val reduce_by_predicate :
Abstract_domain.Logic.eval_env ->
bool ->
Cil_types.predicate Cil_types.named -> Abstract_domain.Logic.eval_env
end