package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-e-acsl.core/E_ACSL/Functions/Libc/index.html

Module `Functions.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.exp -> bool

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

val is_memset : Frama_c_kernel.Cil_types.exp -> bool

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

val is_vla_free : Frama_c_kernel.Cil_types.exp -> bool

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

val get_printf_argument_str : 
  loc:Frama_c_kernel.Cil_types.location ->
  string ->
  Frama_c_kernel.Cil_types.exp list ->
  Frama_c_kernel.Cil_types.exp

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