cprover
|
#include "ansi_c_internal_additions.h"
#include <util/c_types.h>
#include <util/config.h>
#include <goto-programs/adjust_float_expressions.h>
#include <linking/static_lifetime_init.h>
#include "ansi_c_parser.h"
#include "compiler_headers/gcc_builtin_headers_types.inc"
#include "compiler_headers/gcc_builtin_headers_generic.inc"
#include "compiler_headers/gcc_builtin_headers_math.inc"
#include "compiler_headers/gcc_builtin_headers_mem_string.inc"
#include "compiler_headers/gcc_builtin_headers_omp.inc"
#include "compiler_headers/gcc_builtin_headers_tm.inc"
#include "compiler_headers/gcc_builtin_headers_ubsan.inc"
#include "compiler_headers/gcc_builtin_headers_ia32.inc"
#include "compiler_headers/gcc_builtin_headers_ia32-2.inc"
#include "compiler_headers/gcc_builtin_headers_ia32-3.inc"
#include "compiler_headers/gcc_builtin_headers_ia32-4.inc"
#include "compiler_headers/gcc_builtin_headers_ia32-5.inc"
#include "compiler_headers/gcc_builtin_headers_ia32-6.inc"
#include "compiler_headers/gcc_builtin_headers_alpha.inc"
#include "compiler_headers/gcc_builtin_headers_arm.inc"
#include "compiler_headers/gcc_builtin_headers_mips.inc"
#include "compiler_headers/gcc_builtin_headers_power.inc"
#include "compiler_headers/arm_builtin_headers.inc"
#include "compiler_headers/cw_builtin_headers.inc"
#include "compiler_headers/clang_builtin_headers.inc"
#include "cprover_builtin_headers.inc"
#include "compiler_headers/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, bool support_float16_type) |
void | ansi_c_architecture_strings (std::string &code) |
void ansi_c_architecture_strings | ( | std::string & | code | ) |
Definition at line 326 of file ansi_c_internal_additions.cpp.
Definition at line 155 of file ansi_c_internal_additions.cpp.
Definition at line 113 of file ansi_c_internal_additions.cpp.
Definition at line 120 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 142 of file ansi_c_internal_additions.cpp.
Definition at line 93 of file ansi_c_internal_additions.cpp.
Definition at line 101 of file ansi_c_internal_additions.cpp.
Definition at line 105 of file ansi_c_internal_additions.cpp.
Definition at line 97 of file ansi_c_internal_additions.cpp.
Definition at line 74 of file ansi_c_internal_additions.cpp.
Definition at line 79 of file ansi_c_internal_additions.cpp.
Definition at line 25 of file ansi_c_internal_additions.cpp.
Definition at line 54 of file ansi_c_internal_additions.cpp.
Definition at line 58 of file ansi_c_internal_additions.cpp.
Definition at line 61 of file ansi_c_internal_additions.cpp.
Definition at line 64 of file ansi_c_internal_additions.cpp.
Definition at line 67 of file ansi_c_internal_additions.cpp.
Definition at line 70 of file ansi_c_internal_additions.cpp.
Definition at line 30 of file ansi_c_internal_additions.cpp.
Definition at line 35 of file ansi_c_internal_additions.cpp.
Definition at line 83 of file ansi_c_internal_additions.cpp.
Definition at line 41 of file ansi_c_internal_additions.cpp.
Definition at line 88 of file ansi_c_internal_additions.cpp.
Definition at line 45 of file ansi_c_internal_additions.cpp.
Definition at line 20 of file ansi_c_internal_additions.cpp.
Definition at line 49 of file ansi_c_internal_additions.cpp.
Definition at line 109 of file ansi_c_internal_additions.cpp.