Module `Gui_eval.Make`Source

Parameters

module X : Eva.Analysis.S

Signature

Sourcemodule Analysis = X

Sourcetype ('env, 'expr, 'v) evaluation_functions = {

eval_and_warn : 'env -> 'expr -> 'v * bool * bool;
env : Analysis.Dom.t -> Eva.Callstack.t -> 'env;
equal : 'v -> 'v -> bool;
bottom : 'v;
join : 'v -> 'v -> 'v;
expr_to_gui_selection : 'expr -> Gui_types.gui_selection;
res_to_gui_res : 'expr -> 'v -> Analysis.Val.t Gui_types.gui_res;

}

This is the record that encapsulates all evaluation functions

Source

val lval_as_offsm_ev : 
  (Analysis.Dom.t, Frama_c_kernel.Cil_types.lval, Gui_types.gui_offsetmap_res)
    evaluation_functions

Source

val lval_zone_ev : 
  (Analysis.Dom.t,
    Frama_c_kernel.Cil_types.lval,
    Frama_c_kernel.Locations.Zone.t)
    evaluation_functions

Source

val null_ev : 
  (Analysis.Dom.t, unit, Gui_types.gui_offsetmap_res) evaluation_functions

Source

val exp_ev : 
  (Analysis.Dom.t,
    Frama_c_kernel.Cil_types.exp,
    Analysis.Val.t Frama_c_kernel.Lattice_bounds.or_bottom)
    evaluation_functions

Source

val lval_ev : 
  (Analysis.Dom.t,
    Frama_c_kernel.Cil_types.lval,
    Analysis.Val.t Eva.Eval.flagged_value)
    evaluation_functions

Evaluation of logic-originating objects is parameterized by a location information, which is used to build the evaluation environment

Source

val tlval_ev : 
  Gui_types.gui_loc ->
  (Eva__.Eval_terms.eval_env,
    Frama_c_kernel.Cil_types.term,
    Gui_types.gui_offsetmap_res)
    evaluation_functions

Source

val tlval_zone_ev : 
  Gui_types.gui_loc ->
  (Eva__.Eval_terms.eval_env,
    Frama_c_kernel.Cil_types.term,
    Frama_c_kernel.Locations.Zone.t)
    evaluation_functions

Source

val term_ev : 
  Gui_types.gui_loc ->
  (Eva__.Eval_terms.eval_env,
    Frama_c_kernel.Cil_types.term,
    Analysis.Val.t Frama_c_kernel.Lattice_bounds.or_bottom)
    evaluation_functions

Source

val predicate_ev : 
  Gui_types.gui_loc ->
  (Eva__.Eval_terms.eval_env,
    Frama_c_kernel.Cil_types.predicate,
    Frama_c_kernel.Abstract_interp.Comp.result
      Frama_c_kernel.Lattice_bounds.or_bottom)
    evaluation_functions

Source

val predicate_with_red : 
  Gui_types.gui_loc ->
  (Eva__.Eval_terms.eval_env
   * (Frama_c_kernel.Cil_types.kinstr * Eva.Callstack.t),
    Eva__.Red_statuses.alarm_or_property * Frama_c_kernel.Cil_types.predicate,
    Frama_c_kernel.Abstract_interp.Comp.result
      Frama_c_kernel.Lattice_bounds.or_bottom)
    evaluation_functions

Source

val make_data_all_callstacks : 
  ('a, 'b, 'c) evaluation_functions ->
  Gui_types.gui_loc ->
  'b ->
  (Gui_types.gui_callstack * Analysis.Val.t gui_selection_data) list * exn list

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Gui_eval.Make`Source

Parameters

Signature

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Gui_eval.MakeSource

Parameters

Signature

Module `Gui_eval.Make`Source