Analysis (frama-c-eva.Eva_gui.Gui

module Ctx : sig ... end

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 -> Eva.Eval.exp -> Val.t Eva.Eval.evaluated

val copy_lvalue : 
  Dom.state ->
  Eva.Eval.lval ->
  Val.t Eva.Eval.flagged_value Eva.Eval.evaluated

val eval_lval_to_loc : 
  Dom.state ->
  Eva.Eval.lval ->
  Loc.location Eva.Eval.evaluated

val eval_function_exp : 
  Dom.state ->
  ?args:Eva.Eval.exp list ->
  Eva.Eval.exp ->
  Frama_c_kernel.Cil_types.kernel_function list Eva.Eval.evaluated

val assume_cond : 
  Frama_c_kernel.Cil_types.stmt ->
  Dom.state ->
  Eva.Eval.exp ->
  bool ->
  Dom.state Eva.Eval.or_bottom