package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 : 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.

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

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

type 'a gui_selection_data = {
  1. alarm : bool;
  2. red : bool;
  3. before : 'a Gui_types.gui_res;
  4. before_string : string Stdlib.Lazy.t;
  5. after : 'a Gui_types.gui_after;
  6. after_string : string Stdlib.Lazy.t;
}
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 (X : Eva.Analysis.S) : S with module Analysis = X