#include "ansi_c_internal_additions.h"
#include <util/c_types.h>
#include <util/config.h>
#include <linking/static_lifetime_init.h>
#include <goto-programs/adjust_float_expressions.h>
#include "gcc_builtin_headers_types.inc"
#include "gcc_builtin_headers_generic.inc"
#include "gcc_builtin_headers_math.inc"
#include "gcc_builtin_headers_mem_string.inc"
#include "gcc_builtin_headers_omp.inc"
#include "gcc_builtin_headers_tm.inc"
#include "gcc_builtin_headers_ubsan.inc"
#include "gcc_builtin_headers_ia32.inc"
#include "gcc_builtin_headers_ia32-2.inc"
#include "gcc_builtin_headers_ia32-3.inc"
#include "gcc_builtin_headers_ia32-4.inc"
#include "gcc_builtin_headers_ia32-5.inc"
#include "gcc_builtin_headers_alpha.inc"
#include "gcc_builtin_headers_arm.inc"
#include "gcc_builtin_headers_mips.inc"
#include "gcc_builtin_headers_power.inc"
#include "arm_builtin_headers.inc"
#include "cw_builtin_headers.inc"
#include "clang_builtin_headers.inc"
#include "cprover_builtin_headers.inc"
#include "windows_builtin_headers.inc"

Include dependency graph for ansi_c_internal_additions.cpp:

Functions
static std::string	architecture_string (const std::string &value, const char *s)

template<typename T >
static std::string	architecture_string (T value, const char *s)

static mp_integer	max_malloc_size (std::size_t pointer_width, std::size_t object_bits)
	The maximum allocation size is determined by the number of bits that are left in the pointer of width `pointer_width`. More...

void	ansi_c_internal_additions (std::string &code)

void	ansi_c_architecture_strings (std::string &code)

Variables
const char	gcc_builtin_headers_types []

const char	gcc_builtin_headers_generic []

const char	gcc_builtin_headers_math []

const char	gcc_builtin_headers_mem_string []

const char	gcc_builtin_headers_omp [] = "#line 1 \"gcc_builtin_headers_omp.h\"\n"

const char	gcc_builtin_headers_tm [] = "#line 1 \"gcc_builtin_headers_tm.h\"\n"

const char	gcc_builtin_headers_ubsan []

const char	gcc_builtin_headers_ia32 []

const char	gcc_builtin_headers_ia32_2 [] =

const char	gcc_builtin_headers_ia32_3 [] =

const char	gcc_builtin_headers_ia32_4 [] =

const char	gcc_builtin_headers_ia32_5 [] =

const char	gcc_builtin_headers_alpha []

const char	gcc_builtin_headers_arm [] = "#line 1 \"gcc_builtin_headers_arm.h\"\n"

const char	gcc_builtin_headers_mips []

const char	gcc_builtin_headers_power []

const char	arm_builtin_headers [] = "#line 1 \"arm_builtin_headers.h\"\n"

const char	cw_builtin_headers [] = "#line 1 \"cw_builtin_headers.h\"\n"

const char	clang_builtin_headers [] = "#line 1 \"clang_builtin_headers.h\"\n"

const char	cprover_builtin_headers [] = "#line 1 \"cprover_builtin_headers.h\"\n"

const char	windows_builtin_headers [] = "#line 1 \"windows_builtin_headers.h\"\n"

Function Documentation

◆ ansi_c_architecture_strings()

void ansi_c_architecture_strings ( std::string & code )

Definition at line 315 of file ansi_c_internal_additions.cpp.

◆ ansi_c_internal_additions()

void ansi_c_internal_additions ( std::string & code )

Definition at line 148 of file ansi_c_internal_additions.cpp.

◆ architecture_string() [1/2]

static std::string architecture_string	(	const std::string &	value,
		const char *	s
	)

static

Definition at line 107 of file ansi_c_internal_additions.cpp.

◆ architecture_string() [2/2]

template<typename T >

static std::string architecture_string	(	T	value,
		const char *	s
	)

static

Definition at line 114 of file ansi_c_internal_additions.cpp.

◆ max_malloc_size()

static mp_integer max_malloc_size	(	std::size_t	pointer_width,
		std::size_t	object_bits
	)

static

The maximum allocation size is determined by the number of bits that are left in the pointer of width pointer_width.

The allocation size cannot exceed the number represented by the (signed) offset, otherwise it would not be possible to store a pointer into a valid bit of memory. Therefore, the max allocation size is 2^(offset_bits - 1), where the offset bits is the number of bits left in the pointer after the object bits.

The offset must be signed, as a pointer can point to the end of the memory block, and needs to be able to point back to the start.

Parameters