Module Frama_c_kernel.Va_types

type variadic_class =
  1. | Unknown
    (*

    Function declared and not known by Frama-C

    *)
  2. | Builtin
    (*

    Function registered as a builtin function in Cil_builtins

    *)
  3. | Defined
    (*

    Function for which we have the definition in the project

    *)
  4. | Misc
    (*

    Function from the Frama-C lib

    *)
  5. | Overload of overload
    (*

    Function from the Frama-C lib which declines into a finite number of possible prototypes whose names are given in the list

    *)
  6. | Aggregator of aggregator
    (*

    Function from the Frama-C lib which has a not-variadic equivalent with the variadic part replaced by an array. (The array is the aggregation of the arguments from the variadic part.

    *)
  7. | FormatFun of format_fun
    (*

    Function from the Frama-C lib for which the argument count and type is fixed by a format argument.

    *)
  8. | NoTranslation
    (*

    Function that should not be translated.

    *)
and overload = (Cil_types.typ list * Cil_types.varinfo) list
and aggregator = {
  1. a_target : Cil_types.varinfo;
  2. a_pos : int;
  3. a_type : aggregator_type;
  4. a_param : string * Cil_types.typ;
}
and aggregator_type =
  1. | EndedByNull
and format_fun = {
  1. f_kind : Format_types.format_kind;
  2. f_buffer : buffer;
  3. f_format_pos : int;
}
and buffer =
  1. | StdIO
    (*

    Standard input/output (stdin/stdout/stderr)

    *)
  2. | Arg of int * int option
  3. | Stream of int
  4. | File of int
  5. | Syslog
type variadic_function = {
  1. vf_decl : Cil_types.varinfo;
  2. vf_original_type : Cil_types.typ;
  3. vf_class : variadic_class;
  4. mutable vf_specialization_count : int;
}