module Va_types:sig
..end
type
variadic_class =
| |
Unknown |
(* | Function declared and not known by Frama-C | *) |
| |
Builtin |
(* | Function registered as a builtin function in Cil_builtins | *) |
| |
Defined |
(* | Function for which we have the definition in the project | *) |
| |
Misc |
(* | Function from the Frama-C lib | *) |
| |
Overload of |
(* | Function from the Frama-C lib which declines into a finite number of possible prototypes whose names are given in the list | *) |
| |
Aggregator of |
(* | 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. | *) |
| |
FormatFun of |
(* | Function from the Frama-C lib for which the argument count and type is fixed by a format argument. | *) |
typeoverload =
(Cil_types.typ list * Cil_types.varinfo) list
type
aggregator = {
|
a_target : |
|
a_pos : |
|
a_type : |
|
a_param : |
}
type
aggregator_type =
| |
EndedByNull |
type
format_fun = {
|
f_kind : |
|
f_buffer : |
|
f_format_pos : |
}
type
buffer =
| |
StdIO |
(* | Standard input/output (stdin/stdout/stderr) | *) |
| |
Arg of |
|||
| |
Stream of |
|||
| |
File of |
|||
| |
Syslog |
type
variadic_function = {
|
vf_decl : |
|
vf_original_type : |
|
vf_class : |
|
mutable vf_specialization_count : |
}