CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
magic.h
Go to the documentation of this file.
1
4
5#ifndef CPROVER_UTIL_MAGIC_H
6#define CPROVER_UTIL_MAGIC_H
7
8#include <cstddef>
9
10const std::size_t CNF_DUMP_BLOCK_SIZE = 4096;
11const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000;
12const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16;
13// Limit the size of strings in traces to 64M chars to avoid memout
14const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26;
15
16// The top end of the range of integers for which dstrings are precomputed
17constexpr std::size_t DSTRING_NUMBERS_MAX = 64;
18
22
23#endif
const std::size_t CNF_DUMP_BLOCK_SIZE
Definition magic.h:10
constexpr std::size_t DSTRING_NUMBERS_MAX
Definition magic.h:17
const std::size_t MAX_CONCRETE_STRING_SIZE
Definition magic.h:14
constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
Limit the size of arrays for which field_sensitivity gets applied.
Definition magic.h:21
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH
Definition magic.h:12
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition magic.h:11