E_ACSL.Analyses_datatype
Datatypes for analyses types
module Annotation_kind :
Frama_c_kernel.Datatype.S with type t = Analyses_types.annotation_kind
module Pred_or_term :
Frama_c_kernel.Datatype.S_with_collections
with type t = Analyses_types.pred_or_term
module At_data : sig ... end
module Ival_datatype :
Frama_c_kernel.Datatype.S_with_collections with type t = Analyses_types.ival
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
module Id_term_in_profile :
Frama_c_kernel.Datatype.S_with_collections
with type t = Frama_c_kernel.Cil_types.term * Profile.t
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.
module LFProf :
Frama_c_kernel.Datatype.S_with_collections
with type t = Frama_c_kernel.Cil_types.logic_info * Profile.t
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 the fixpoint algorithm for recursive functions
module Number_ty :
Frama_c_kernel.Datatype.S_with_collections
with type t = Analyses_types.number_ty