Analyses_datatype (frama-c-e-acsl.E_ACSL.Analyses

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

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 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_hashtbl
    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 fixpoint algorithm for recursive functions. This environment 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