Frama-C API - Analyses_datatype
Datatypes for analyses types
module Annotation_kind : Frama_c_kernel.Datatype.S with type t = Analyses_types.annotation_kindmodule Pred_or_term : Frama_c_kernel.Datatype.S_with_collections with type t = Analyses_types.pred_or_termPredicate 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 ... endmodule Ival_datatype : Frama_c_kernel.Datatype.S_with_collections with type t = Analyses_types.ivalmodule Profile : sig ... endprofile that maps logic variables that are function parameters to their interval depending on the arguments at the callsite of the function
module Id_term_in_profile : Frama_c_kernel.Datatype.S_with_collections with type t = Frama_c_kernel.Cil_types.term * Profile.tterm with a profile: a term inside a logic function or predicate may contain free variables. The profile indicates the interval for those free variables.
module LFProf : Frama_c_kernel.Datatype.S_with_collections with type t = Frama_c_kernel.Cil_types.logic_info * Profile.tprofile 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 ... endlogic environment: interval of all bound variables. It consists in two components
module LF_env : sig ... endImperative environment to perform fixpoint algorithm for recursive functions. This environnement store four pieces of information associated to every logic_info:
module Number_ty : Frama_c_kernel.Datatype.S_with_collections with type t = Analyses_types.number_ty