ROSE  0.11.51.0
Public Types | Public Attributes | List of all members
Rose::BinaryAnalysis::ModelChecker::P2Model::Settings Struct Reference

Description

Settings for this model.

Definition at line 31 of file P2Model.h.

#include <P2Model.h>

Collaboration diagram for Rose::BinaryAnalysis::ModelChecker::P2Model::Settings:
Collaboration graph
[legend]

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...
 
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 = true
 Whether the SMT solver should use memoization. More...
 
bool traceSemantics = false
 Whether to trace all RISC operators. More...
 

Member Enumeration Documentation

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.

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

Maximum address of the null page.

Definition at line 42 of file P2Model.h.

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

Address for initial stack pointer.

Definition at line 44 of file P2Model.h.

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

Type of memory state.

Definition at line 45 of file P2Model.h.

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

Whether the SMT solver should use memoization.

Definition at line 46 of file P2Model.h.

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

Whether to trace all RISC operators.

Definition at line 47 of file P2Model.h.


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