Frama-C:
Plug-ins:
Libraries:

Frama-C API - Analyses_datatype

Datatypes for analyses types

Predicate or term. Note that the notion of egality for predicates is structural but for terms it is physical (using Misc.Id_term). That means that comparison is undefined and that Map and Set cannot be used. See Misc.Id_term for more information.

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: