ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
builtin_names.h File Reference
#include <util/symtab/context.h>
#include <util/irep/irep.h>
#include <string>
Include dependency graph for builtin_names.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Enumerations

enum class  ieee_float_builtin { none , nearbyint , remainder , fma }
 The float library calls that have an IEEE node of their own. More...

Functions

bool compare_float_suffix (const irep_idt &identifier, const std::string &name)
 Callee-name matching shared by clang_c_adjust::do_special_functions and its IREP2 counterpart.
bool compare_unscore_builtin (const irep_idt &identifier, const std::string &name)
 name and its __- and __builtin_-prefixed spellings, each with the float suffixes: isnan, __isnanf, __builtin_isnanl, ...
bool is_abs_builtin_name (const irep_idt &identifier)
 True for the abs builtins that may be lowered to an abs node.
ieee_float_builtin ieee_float_builtin_of (const irep_idt &identifier)
bool is_name_matched_builtin (const irep_idt &identifier)
 The lowerings that match a callee's base name, so a program that defines one of these names itself would have its body discarded and the builtin verified in its place (#6904).
bool builtin_shadows_user_definition (const contextt &context, const irep_idt &base_name, const irep_idt &symbol_id)
 True when lowering this call would throw away a definition the program supplies.

Enumeration Type Documentation

◆ ieee_float_builtin

enum class ieee_float_builtin
strong

The float library calls that have an IEEE node of their own.

Both passes lower these, so the spelling set is shared; the arity each node takes is not, because legacy splices whatever arguments the call has into a fixed-arity node (see clang_c_adjust_irep2.cpp).

Enumerator
none 
nearbyint 
remainder 
fma 

Function Documentation

◆ builtin_shadows_user_definition()

bool builtin_shadows_user_definition ( const contextt & context,
const irep_idt & base_name,
const irep_idt & symbol_id )

True when lowering this call would throw away a definition the program supplies.

Libc's own declarations are bodiless, and the <cmath> overloads forward to a spelling that lowers in their place – the __builtin_ one for most, the f/l suffixes for fma (src/cpp/library/cmath) – so a std:: call still reaches a node, one frame further in.

Parameters
base_namethe spelling the lowerings match on
symbol_idthe callee's linkage identifier, which is what the symbol table is keyed by

◆ compare_float_suffix()

bool compare_float_suffix ( const irep_idt & identifier,
const std::string & name )

Callee-name matching shared by clang_c_adjust::do_special_functions and its IREP2 counterpart.

Both lower the same builtins, so both must agree on which spellings are one; a second copy of these predicates is exactly the shape of divergence unit/util/c_typecast.test.cpp exists to catch elsewhere. name, namef, named, namel.

◆ compare_unscore_builtin()

bool compare_unscore_builtin ( const irep_idt & identifier,
const std::string & name )

name and its __- and __builtin_-prefixed spellings, each with the float suffixes: isnan, __isnanf, __builtin_isnanl, ...

◆ ieee_float_builtin_of()

ieee_float_builtin ieee_float_builtin_of ( const irep_idt & identifier)

◆ is_abs_builtin_name()

bool is_abs_builtin_name ( const irep_idt & identifier)

True for the abs builtins that may be lowered to an abs node.

That node becomes (x >= 0) ? x : -x, ill-typed for anything but an arithmetic argument, so a program overloading the name for a class type – std::abs(complex) is why <complex> ships without it – keeps its call.

◆ is_name_matched_builtin()

bool is_name_matched_builtin ( const irep_idt & identifier)

The lowerings that match a callee's base name, so a program that defines one of these names itself would have its body discarded and the builtin verified in its place (#6904).

These are all spellings a program is free to reuse – mylib::abs, mylib::isinf – unlike the __builtin_-prefixed and CPROVER-prefixed entries, which are reserved.