S.Analysis
module Val : sig ... end
module Loc : sig ... end
module Dom : sig ... end
module Eval : sig ... end
include Eva.Analysis.Results
with type state := Dom.state
and type value := Val.t
and type location := Loc.location
val get_global_state : unit -> Dom.state Eva.Eval.or_top_bottom
val get_stmt_state :
after:bool ->
Frama_c_kernel.Cil_types.stmt ->
Dom.state Eva.Eval.or_top_bottom
val get_stmt_state_by_callstack :
?selection:Eva.Callstack.t list ->
after:bool ->
Frama_c_kernel.Cil_types.stmt ->
Dom.state Eva.Callstack.Hashtbl.t Eva.Eval.or_top_bottom
val get_initial_state :
Frama_c_kernel.Cil_types.kernel_function ->
Dom.state Eva.Eval.or_top_bottom
val get_initial_state_by_callstack :
?selection:Eva.Callstack.t list ->
Frama_c_kernel.Cil_types.kernel_function ->
Dom.state Eva.Callstack.Hashtbl.t Eva.Eval.or_top_bottom
val eval_expr :
Dom.state ->
Frama_c_kernel.Cil_types.exp ->
Val.t Eva.Eval.evaluated
val copy_lvalue :
Dom.state ->
Frama_c_kernel.Cil_types.lval ->
Val.t Eva.Eval.flagged_value Eva.Eval.evaluated
val eval_lval_to_loc :
Dom.state ->
Frama_c_kernel.Cil_types.lval ->
Loc.location Eva.Eval.evaluated
val eval_function_exp :
Dom.state ->
?args:Frama_c_kernel.Cil_types.exp list ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.kernel_function list Eva.Eval.evaluated
val assume_cond :
Frama_c_kernel.Cil_types.stmt ->
Dom.state ->
Frama_c_kernel.Cil_types.exp ->
bool ->
Dom.state Eva.Eval.or_bottom