CBMC
magic.h
Go to the documentation of this file.
1
5
#ifndef CPROVER_UTIL_MAGIC_H
6
#define CPROVER_UTIL_MAGIC_H
7
8
#include <cstddef>
9
10
const
std::size_t
CNF_DUMP_BLOCK_SIZE
= 4096;
11
const
std::size_t
MAX_FLATTENED_ARRAY_SIZE
=1000;
12
const
std::size_t
STRING_REFINEMENT_MAX_CHAR_WIDTH
= 16;
13
// Limit the size of strings in traces to 64M chars to avoid memout
14
const
std::size_t
MAX_CONCRETE_STRING_SIZE
= 1 << 26;
15
16
// The top end of the range of integers for which dstrings are precomputed
17
constexpr std::size_t
DSTRING_NUMBERS_MAX
= 64;
18
21
constexpr std::size_t
DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
= 64;
22
23
#endif
MAX_FLATTENED_ARRAY_SIZE
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition:
magic.h:11
MAX_CONCRETE_STRING_SIZE
const std::size_t MAX_CONCRETE_STRING_SIZE
Definition:
magic.h:14
DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
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
CNF_DUMP_BLOCK_SIZE
const std::size_t CNF_DUMP_BLOCK_SIZE
Definition:
magic.h:10
STRING_REFINEMENT_MAX_CHAR_WIDTH
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH
Definition:
magic.h:12
DSTRING_NUMBERS_MAX
constexpr std::size_t DSTRING_NUMBERS_MAX
Definition:
magic.h:17
src
util
magic.h
Generated by
1.8.17