#include <string_view>
#include <util/base/prefix.h>

Include dependency graph for c_builtins.h:

This graph shows which files directly or indirectly include this file:

Enumerations
enum class	bit_scan_endt { none , leading , trailing , first_set , redundant_sign }
	Which bit of the operand a __builtin_clz‍/ctz‍/ffs‍/clrsb call reports. More...

Functions
bit_scan_endt	bit_scan_builtin (std::string_view symname)
	Recognise the __builtin_clz‍/__builtin_ctz family from a symbol name such as "c:@F@__builtin_clzll".

Variables
constexpr int	esbmc_object_size_whole = 4
	An __ESBMC_builtin_object_size type outside GCC's 0..3: the size of the whole object, regardless of the pointer's offset, which is what CBMC's __CPROVER_OBJECT_SIZE and r_ok/w_ok extents mean (#8660).

Enumeration Type Documentation

◆ bit_scan_endt

enum class bit_scan_endt

strong

Which bit of the operand a __builtin_clz*‍/ctz*‍/ffs*‍/clrsb* call reports.

Enumerator
none
leading
trailing
first_set	ffs: the one-based index of the least-significant set bit, and 0 for a zero operand – defined there, unlike the other two.
redundant_sign	clrsb: the leading bits equal to the sign bit, less the sign bit itself; defined for every operand.

Function Documentation

◆ bit_scan_builtin()

bit_scan_endt bit_scan_builtin ( std::string_view symname )

inline

Recognise the __builtin_clz*‍/__builtin_ctz* family from a symbol name such as "c:@F@__builtin_clzll".

The type-generic g spellings take an optional second argument, the result to use when the operand is zero – which is what makes them defined there, unlike the rest of the family (GCC, "Bit Operation Builtins").

The width suffix is matched against a closed set rather than by prefix: a loose "__builtin_clz" test would also capture unrelated builtins that happen to start the same way, which is how the two-argument clzg once reached a one-argument handler (#4606).

Variable Documentation

◆ esbmc_object_size_whole

int esbmc_object_size_whole = 4

constexpr

An __ESBMC_builtin_object_size type outside GCC's 0..3: the size of the whole object, regardless of the pointer's offset, which is what CBMC's __CPROVER_OBJECT_SIZE and r_ok/w_ok extents mean (#8660).

Enumerations