CBMC
magic.h File Reference

Magic numbers used throughout the codebase. More...

#include <cstddef>
+ Include dependency graph for magic.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Variables

const std::size_t CNF_DUMP_BLOCK_SIZE = 4096
 
const std::size_t MAX_FLATTENED_ARRAY_SIZE =1000
 
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16
 
const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26
 
constexpr std::size_t DSTRING_NUMBERS_MAX = 64
 
constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE = 64
 Limit the size of arrays for which field_sensitivity gets applied. More...
 

Detailed Description

Magic numbers used throughout the codebase.

Author
Kareem Khazem karkh.nosp@m.az@k.nosp@m.arkha.nosp@m.z.co.nosp@m.m

Definition in file magic.h.

Variable Documentation

◆ CNF_DUMP_BLOCK_SIZE

const std::size_t CNF_DUMP_BLOCK_SIZE = 4096

Definition at line 10 of file magic.h.

◆ DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE

constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE = 64
constexpr

Limit the size of arrays for which field_sensitivity gets applied.

Necessary because large constant arrays slow-down the process.

Definition at line 21 of file magic.h.

◆ DSTRING_NUMBERS_MAX

constexpr std::size_t DSTRING_NUMBERS_MAX = 64
constexpr

Definition at line 17 of file magic.h.

◆ MAX_CONCRETE_STRING_SIZE

const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26

Definition at line 14 of file magic.h.

◆ MAX_FLATTENED_ARRAY_SIZE

const std::size_t MAX_FLATTENED_ARRAY_SIZE =1000

Definition at line 11 of file magic.h.

◆ STRING_REFINEMENT_MAX_CHAR_WIDTH

const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16

Definition at line 12 of file magic.h.