Rose::BinaryAnalysis::ModelChecker::P2Model::Settings Struct Reference

Description

Settings for this model.

Definition at line 31 of file P2Model.h.

#include <Rose/BinaryAnalysis/ModelChecker/P2Model.h>

Collaboration diagram for Rose::BinaryAnalysis::ModelChecker::P2Model::Settings:

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...

Member Enumeration Documentation

enum Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::MemoryType

strong

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 P2Model.h.

Member Data Documentation

TestMode Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::nullRead = TestMode::MUST

How to test for reads from the null page.

Definition at line 38 of file P2Model.h.

TestMode Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::nullWrite = TestMode::MUST

How to test for writes from the null page.

Definition at line 39 of file P2Model.h.

TestMode Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::oobRead = TestMode::OFF

How to test for out-of-bounds reads.

Definition at line 40 of file P2Model.h.

TestMode Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::oobWrite = TestMode::OFF

How to test for out-of-bounds writes.

Definition at line 41 of file P2Model.h.

TestMode Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::uninitVar = TestMode::OFF

How to test for uninitialized variable reads.

Definition at line 42 of file P2Model.h.

rose_addr_t Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::maxNullAddress = 4095

Maximum address of the null page.

Definition at line 43 of file P2Model.h.

Sawyer::Optional<rose_addr_t> Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::initialStackVa

Address for initial stack pointer.

Definition at line 45 of file P2Model.h.

MemoryType Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::memoryType = MemoryType::MAP

Type of memory state.

Definition at line 46 of file P2Model.h.

bool Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::solverMemoization = false

Whether the SMT solver should use memoization.

Definition at line 47 of file P2Model.h.

bool Rose::BinaryAnalysis::ModelChecker::P2Model::Settings::traceSemantics = false

Whether to trace all RISC operators.

Definition at line 48 of file P2Model.h.

---

The documentation for this struct was generated from the following file:

• P2Model.h