This data structure supports saving partially-executed symbolic execution paths so that their execution can be halted and resumed later. The choice of which path should be resumed next is implemented by subtypes of this abstract class.

Definition at line 37 of file path_storage.h.

Member Typedef Documentation

◆ name_index_mapt

typedef std::unordered_map<irep_idt, std::size_t> path_storaget::name_index_mapt

private

Definition at line 145 of file path_storage.h.

Constructor & Destructor Documentation

◆ ~path_storaget()

virtual path_storaget::~path_storaget ( )

virtualdefault

Member Function Documentation

◆ add_function_loops()

void path_storaget::add_function_loops ( const irep_idt & identifier,

const goto_programt & body

)

inline

Generates a loop analysis for the instructions in goto_programt and keys it against function ID.

Definition at line 120 of file path_storage.h.

◆ clear()

virtual void path_storaget::clear ( )

pure virtual

Clear all saved paths.

This is typically used because we want to terminate symbolic execution early. It doesn't matter too much in terms of memory usage since CBMC typically exits soon after we do that, however it's nice to have tests that check that the worklist is always empty when symex finishes.

Implemented in path_lifot, and path_fifot.

◆ empty()

bool path_storaget::empty ( ) const

inline

Is this storage empty?

Definition at line 88 of file path_storage.h.

◆ get_loop_analysis()

std::shared_ptr< lexical_loopst > path_storaget::get_loop_analysis ( const irep_idt & function_id )

inline

Definition at line 131 of file path_storage.h.

◆ get_unique_index()

std::size_t path_storaget::get_unique_index ( name_index_mapt & unique_index_map,

const irep_idt & id,

std::size_t minimum_index

)

inlineprivate

Definition at line 147 of file path_storage.h.

◆ get_unique_l1_index()

std::size_t path_storaget::get_unique_l1_index ( const irep_idt & id,

std::size_t minimum_index

)

inline

Provide a unique L1 index for a given id, starting from minimum_index.

Definition at line 104 of file path_storage.h.

◆ get_unique_l2_index()

std::size_t path_storaget::get_unique_l2_index ( const irep_idt & id )

inline

Definition at line 109 of file path_storage.h.

◆ peek()

patht & path_storaget::peek ( )

inline

Reference to the next path to resume.

Definition at line 60 of file path_storage.h.

◆ pop()

void path_storaget::pop ( )

inline

Remove the next path to resume from the storage.

Definition at line 78 of file path_storage.h.

◆ private_peek()

virtual patht & path_storaget::private_peek ( )

privatepure virtual

Implemented in path_lifot, and path_fifot.

◆ private_pop()

virtual void path_storaget::private_pop ( )

privatepure virtual

Implemented in path_lifot, and path_fifot.

◆ push()

virtual void path_storaget::push ( const patht & )

pure virtual

Add a path to resume to the storage.

Implemented in path_lifot, and path_fifot.

◆ size()

virtual std::size_t path_storaget::size ( ) const

pure virtual

How many paths does this storage contain?

Implemented in path_lifot, and path_fifot.

Member Data Documentation

◆ build_symex_nondet

symex_nondet_generatort path_storaget::build_symex_nondet

Counter for nondet objects, which require unique names.

Definition at line 94 of file path_storage.h.

◆ dirty

incremental_dirtyt path_storaget::dirty

Local variables are considered 'dirty' if they've had an address taken and therefore may be referred to by a pointer.

Definition at line 116 of file path_storage.h.

◆ l1_indices

name_index_mapt path_storaget::l1_indices

private

Storage used by get_unique_index.

Definition at line 161 of file path_storage.h.

◆ l2_indices

name_index_mapt path_storaget::l2_indices

private

Definition at line 162 of file path_storage.h.

◆ loop_analysis_map

std::unordered_map<irep_idt, std::shared_ptr<lexical_loopst> > path_storaget::loop_analysis_map

private

Definition at line 138 of file path_storage.h.

◆ safe_pointers

std::unordered_map<irep_idt, local_safe_pointerst> path_storaget::safe_pointers

Map function identifiers to local_safe_pointerst instances.

This is to identify derferences that are guaranteed to be safe in a given execution context, thus helping to avoid symex to follow spurious error-handling paths.

Definition at line 100 of file path_storage.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/path_storage.h