Frama-C:
Plug-ins:
Libraries:

Frama-C API - Libc

val has_replacement : string -> bool

Given 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 -> string

Given the name of C library function return the name of the RTL function that potentially replaces it.

val is_memcpy : Frama_c_kernel.Cil_types.lhost -> bool

Return true if lhost captures a function name that matches memcpy or an equivalent function.

  • before 32.0-Germanium

    Function parameter was an expression.

val is_memset : Frama_c_kernel.Cil_types.lhost -> bool

Return true if lhost captures a function name that matches memset or an equivalent function.

  • before 32.0-Germanium

    Function parameter was an expression.

val is_vla_free : Frama_c_kernel.Cil_types.lhost -> bool

Return true if lhost captures a function name that matches a function that allocates memory for a variable-size array..

  • before 32.0-Germanium

    Function parameter was an expression.

val is_vla_free_name : string -> bool

Return 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 -> bool

Same as is_dyn_alloc but for strings

val is_printf_name : string -> bool

Same as is_printf but for strings

Given 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:

  • "b" -> _Bool
  • "c" -> signed char
  • "C" -> unsigned char
  • "d" -> int
  • "D" -> unsigned int
  • "h" -> short
  • "H" -> unsigned short
  • "l" -> long
  • "L" -> unsigned long
  • "r" -> long long
  • "R" -> unsigned long long
  • "f" -> float
  • "e" -> double
  • "E" -> long double
  • "s" -> char*
  • "i" -> int*
  • "p" -> void*
val actual_alloca : string

The name of an actual alloca function used at link-time. In GCC/Clang alloca is typically implemented via __builtin_alloca