Module `Eva_gui.Gui_eval`Source

This module defines an abstraction to evaluate various things across multiple callstacks. Currently, l-values, NULL, expressions, term-lvalues, terms and predicates can be evaluated

Sourceval results_kf_computed : Frama_c_kernel.Cil_types.kernel_function -> bool

Catch the fact that we are in a function for which -no-results or one of its variants is set. Without this check, we would display much non-sensical information.

Source

val classify_pre_post : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Property.t ->
  Gui_types.gui_loc option

State in which the predicate, found in the given function, should be evaluated

Sourceval gui_loc_logic_env : Gui_types.gui_loc -> Frama_c_kernel.Logic_typing.Lenv.t

Logic labels valid at the given location. C labels are _not_ added, even if the location is a statement.

Sourcetype 'a gui_selection_data = {

alarm : bool;
red : bool;
before : 'a Gui_types.gui_res;
before_string : string Lazy.t;
after : 'a Gui_types.gui_after;
after_string : string Lazy.t;

}

Sourceval gui_selection_data_empty : 'a gui_selection_data

Default value. All the fields contain empty or dummy values

Sourcemodule type S = sig ... end

The types and function below depend on the abstract domains and values currently available in Eva.

Sourcemodule Make (X : Eva.Analysis.S) : S with module Analysis = X

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Eva_gui.Gui_eval`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Eva_gui.Gui_evalSource

Module `Eva_gui.Gui_eval`Source