module Gui_eval: sig
.. end
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
val results_kf_computed : 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.
val classify_pre_post : Cil_types.kernel_function -> Property.t -> Gui_types.gui_loc option
State in which the predicate, found in the given function,
should be evaluated
val gui_loc_logic_env : Gui_types.gui_loc -> Logic_typing.Lenv.t
Logic labels valid at the given location. C labels are _not_ added,
even if the location is a statement.
type 'a
gui_selection_data = {
}
val gui_selection_data_empty : 'a gui_selection_data
Default value. All the fields contain empty or dummy values
module type S = sig
.. end
The types and function below depend on the abstract domains and values
currently available in Eva.
module Make: