module type Logic = sig
.. end
Logic evaluation. Temporary API.
TODO: factorization of these functions for generic abstract domain.
type
state
type
eval_env
Evaluation environment.
val env_current_state : eval_env -> state Eval.or_bottom
val env_annot : pre:state ->
here:state -> unit -> eval_env
val env_pre_f : pre:state -> unit -> eval_env
val env_post_f : pre:state ->
post:state ->
result:Cil_types.varinfo option -> unit -> eval_env
val eval_predicate : eval_env -> Cil_types.predicate -> Alarmset.status
val reduce_by_predicate : eval_env ->
bool -> Cil_types.predicate -> eval_env