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 Lazy.t;
  5. after : 'a Gui_types.gui_after;
  6. after_string : string 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct