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