Parameter `Make.X`

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-eva.gui/Eva_gui/Gui_eval/Make/argument-1-X/index.html

Parameter `Make.X`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-eva.gui/Eva_gui/Gui_eval/Make/argument-1-X/index.html

Parameter Make.X

Parameter `Make.X`