package frama-c

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

Datatypes for analyses types

module At_data : sig ... end
module Profile : sig ... end

profile that maps logic variables that are function parameters to their interval depending on the arguments at the callsite of the function

term with a profile: a term inside a logic function or predicate may contain free variables. The profile indicates the interval for those free variables.

profile of logic function or predicate: a logic info representing a logic function or a predicate together with a profile for its arguments.

module Logic_env : sig ... end

logic environment: interval of all bound variables. It consists in two components

module LF_env : sig ... end

Imperative environment to perform fixpoint algorithm for recursive functions. This environnement store four pieces of information associated to every logic_info: