cprover
|
#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"
Go to the source code of this file.
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 . | |
void | ansi_c_internal_additions (std::string &code) |
void | ansi_c_architecture_strings (std::string &code) |
void ansi_c_architecture_strings | ( | std::string & | code | ) |
Definition at line 301 of file ansi_c_internal_additions.cpp.
void ansi_c_internal_additions | ( | std::string & | code | ) |
Definition at line 148 of file ansi_c_internal_additions.cpp.
Definition at line 107 of file ansi_c_internal_additions.cpp.
Definition at line 114 of file ansi_c_internal_additions.cpp.
|
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.
pointer_width | The width of the pointer |
object_bits | : The number of bits used to represent the ID |
Definition at line 135 of file ansi_c_internal_additions.cpp.
const char arm_builtin_headers[] = "#line 1 \"arm_builtin_headers.h\"\n" |
Definition at line 87 of file ansi_c_internal_additions.cpp.
const char clang_builtin_headers[] = "#line 1 \"clang_builtin_headers.h\"\n" |
Definition at line 95 of file ansi_c_internal_additions.cpp.
const char cprover_builtin_headers[] = "#line 1 \"cprover_builtin_headers.h\"\n" |
Definition at line 99 of file ansi_c_internal_additions.cpp.
const char cw_builtin_headers[] = "#line 1 \"cw_builtin_headers.h\"\n" |
Definition at line 91 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_alpha[] |
Definition at line 68 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_arm[] = "#line 1 \"gcc_builtin_headers_arm.h\"\n" |
Definition at line 73 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_generic[] |
Definition at line 23 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_ia32[] |
Definition at line 51 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_ia32_2[] = |
Definition at line 55 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_ia32_3[] = |
Definition at line 58 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_ia32_4[] = |
Definition at line 61 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_ia32_5[] = |
Definition at line 64 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_math[] |
Definition at line 28 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_mem_string[] |
Definition at line 33 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_mips[] |
Definition at line 77 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_omp[] = "#line 1 \"gcc_builtin_headers_omp.h\"\n" |
Definition at line 38 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_power[] |
Definition at line 82 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_tm[] = "#line 1 \"gcc_builtin_headers_tm.h\"\n" |
Definition at line 42 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_types[] |
Definition at line 18 of file ansi_c_internal_additions.cpp.
const char gcc_builtin_headers_ubsan[] |
Definition at line 46 of file ansi_c_internal_additions.cpp.
const char windows_builtin_headers[] = "#line 1 \"windows_builtin_headers.h\"\n" |
Definition at line 103 of file ansi_c_internal_additions.cpp.