ROSE
0.11.102.0
|
Settings for this model.
Definition at line 31 of file PartitionerModel.h.
#include <Rose/BinaryAnalysis/ModelChecker/PartitionerModel.h>
Public Types | |
enum | MemoryType { MemoryType::LIST, MemoryType::MAP } |
Type of memory state to use. More... | |
Public Attributes | |
TestMode | nullRead = TestMode::MUST |
How to test for reads from the null page. More... | |
TestMode | nullWrite = TestMode::MUST |
How to test for writes from the null page. More... | |
TestMode | oobRead = TestMode::OFF |
How to test for out-of-bounds reads. More... | |
TestMode | oobWrite = TestMode::OFF |
How to test for out-of-bounds writes. More... | |
TestMode | uninitVar = TestMode::OFF |
How to test for uninitialized variable reads. More... | |
rose_addr_t | maxNullAddress = 4095 |
Maximum address of the null page. More... | |
bool | debugNull = false |
When debugging is enabled, show null pointer checking? | |
Sawyer::Optional< rose_addr_t > | initialStackVa |
Address for initial stack pointer. More... | |
MemoryType | memoryType = MemoryType::MAP |
Type of memory state. More... | |
bool | solverMemoization = false |
Whether the SMT solver should use memoization. More... | |
bool | traceSemantics = false |
Whether to trace all RISC operators. More... | |
Type of memory state to use.
Enumerator | |
---|---|
LIST |
Reverse chronological list. This is more accurate. |
MAP |
Map indexed by symbolic address hash. This is faster. |
Definition at line 33 of file PartitionerModel.h.
TestMode Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::nullRead = TestMode::MUST |
How to test for reads from the null page.
Definition at line 38 of file PartitionerModel.h.
TestMode Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::nullWrite = TestMode::MUST |
How to test for writes from the null page.
Definition at line 39 of file PartitionerModel.h.
TestMode Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::oobRead = TestMode::OFF |
How to test for out-of-bounds reads.
Definition at line 40 of file PartitionerModel.h.
TestMode Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::oobWrite = TestMode::OFF |
How to test for out-of-bounds writes.
Definition at line 41 of file PartitionerModel.h.
TestMode Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::uninitVar = TestMode::OFF |
How to test for uninitialized variable reads.
Definition at line 42 of file PartitionerModel.h.
rose_addr_t Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::maxNullAddress = 4095 |
Maximum address of the null page.
Definition at line 43 of file PartitionerModel.h.
Sawyer::Optional<rose_addr_t> Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::initialStackVa |
Address for initial stack pointer.
Definition at line 45 of file PartitionerModel.h.
MemoryType Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::memoryType = MemoryType::MAP |
Type of memory state.
Definition at line 46 of file PartitionerModel.h.
bool Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::solverMemoization = false |
Whether the SMT solver should use memoization.
Definition at line 47 of file PartitionerModel.h.
bool Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::traceSemantics = false |
Whether to trace all RISC operators.
Definition at line 48 of file PartitionerModel.h.