CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Attributes | Private Member Functions | List of all members
path_lifot Class Reference

LIFO save queue: depth-first search, try to finish paths. More...

#include <path_storage.h>

+ Inheritance diagram for path_lifot:
[フレーム]
[legend]
+ Collaboration diagram for path_lifot:
[フレーム]
[legend]

Public Member Functions

void  push (const patht &) override
  Add a path to resume to the storage.
 
std::size_t  size () const override
  How many paths does this storage contain?
 
void  clear () override
  Clear all saved paths.
 
- Public Member Functions inherited from path_storaget
virtual  ~path_storaget ()=default
 
patht &  peek ()
  Reference to the next path to resume.
 
void  pop ()
  Remove the next path to resume from the storage.
 
bool  empty () const
  Is this storage empty?
 
std::size_t  get_unique_l1_index (const irep_idt &id, std::size_t minimum_index)
  Provide a unique L1 index for a given id, starting from minimum_index.
 
std::size_t  get_unique_l2_index (const irep_idt &id)
 
void  add_function_loops (const irep_idt &identifier, const goto_programt &body)
  Generates a loop analysis for the instructions in goto_programt and keys it against function ID.
 
std::shared_ptr< lexical_loopst >  get_loop_analysis (const irep_idt &function_id)
 

Protected Attributes

std::list< path_storaget::patht >::iterator  last_peeked
 
std::list< patht >  paths
 

Private Member Functions

patht &  private_peek () override
 
void  private_pop () override
 

Additional Inherited Members

- Public Attributes inherited from path_storaget
symex_nondet_generatort  build_symex_nondet
  Counter for nondet objects, which require unique names.
 
std::unordered_map< irep_idt, local_safe_pointerst >  safe_pointers
  Map function identifiers to local_safe_pointerst instances.
 
incremental_dirtyt  dirty
  Local variables are considered 'dirty' if they've had an address taken and therefore may be referred to by a pointer.
 

Detailed Description

LIFO save queue: depth-first search, try to finish paths.

Definition at line 166 of file path_storage.h.

Member Function Documentation

◆  clear()

void path_lifot::clear ( )
overridevirtual

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.

Implements path_storaget.

Definition at line 51 of file path_storage.cpp.

◆  private_peek()

path_storaget::patht & path_lifot::private_peek ( )
overrideprivatevirtual

Implements path_storaget.

Definition at line 27 of file path_storage.cpp.

◆  private_pop()

void path_lifot::private_pop ( )
overrideprivatevirtual

Implements path_storaget.

Definition at line 39 of file path_storage.cpp.

◆  push()

void path_lifot::push ( const patht &  )
overridevirtual

Add a path to resume to the storage.

Implements path_storaget.

Definition at line 34 of file path_storage.cpp.

◆  size()

std::size_t path_lifot::size ( ) const
overridevirtual

How many paths does this storage contain?

Implements path_storaget.

Definition at line 46 of file path_storage.cpp.

Member Data Documentation

◆  last_peeked

std::list<path_storaget::patht>::iterator path_lifot::last_peeked
protected

Definition at line 174 of file path_storage.h.

◆  paths

std::list<patht> path_lifot::paths
protected

Definition at line 175 of file path_storage.h.

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

AltStyle によって変換されたページ (->オリジナル) /