Frama-C API - X
module Ctx : sig ... endmodule Val : sig ... endmodule Loc : sig ... endmodule Dom : sig ... endmodule Eval : sig ... endinclude 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_bottomval get_stmt_state : after:bool -> Frama_c_kernel.Cil_types.stmt -> Dom.state Eva.Eval.or_top_bottomval 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_bottomval get_initial_state : Frama_c_kernel.Cil_types.kernel_function -> Dom.state Eva.Eval.or_top_bottomval 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_bottomval eval_expr : Dom.state -> Eva.Eval.exp -> Val.t Eva.Eval.evaluatedval copy_lvalue : Dom.state -> Eva.Eval.lval -> Val.t Eva.Eval.flagged_value Eva.Eval.evaluatedval eval_lval_to_loc : Dom.state -> Eva.Eval.lval -> Loc.location Eva.Eval.evaluatedval eval_function_exp : Dom.state -> ?args:Eva.Eval.exp list -> Eva.Eval.exp -> Frama_c_kernel.Cil_types.kernel_function list Eva.Eval.evaluatedval assume_cond : Frama_c_kernel.Cil_types.stmt -> Dom.state -> Eva.Eval.exp -> bool -> Dom.state Eva.Eval.or_bottom