module Libc:sig..end
val has_replacement : string -> boolGiven the name of C library function return true if there is a drop-in replacement function for it in the RTL.
val replacement_name : string -> stringGiven the name of C library function return the name of the RTL function that potentially replaces it.
val is_memcpy : Cil_types.exp -> boolReturn true if exp captures a function name that matches memcpy or
an equivalent function
val is_memset : Cil_types.exp -> boolReturn true if exp captures a function name that matches memset or
an equivalent function
val is_vla_free : Cil_types.exp -> boolReturn true if exp captures a function name that matches
a function that allocates memory for a variable-size array.
val is_vla_free_name : string -> boolReturn true if string captures a function name that matches
a function that deallocates memory for a variable-size array.
val is_vla_alloc_name : string -> boolSame as is_dyn_alloc but for strings
val is_printf_name : string -> boolSame as is_printf but for strings
val get_printf_argument_str : loc:Cil_types.location -> string -> Cil_types.exp list -> Cil_types.expGiven the name of a printf-like function and the list of its variadic arguments return a literal string expression where each character describes the type of an argument from a list. Such characters are also called abbreviated types. Conversion between abbreviated and C types characters is as follows:
_Boolsigned charunsigned charintunsigned intshortunsigned shortlongunsigned longlong longunsigned long longfloatdoublelong doublechar*int*void*val actual_alloca : stringThe name of an actual alloca function used at link-time.
In GCC/Clang alloca is typically implemented via __builtin_alloca