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

FIFO save queue: paths are resumed in the order that they were saved. More...

#include <path_storage.h>

+ Inheritance diagram for path_fifot:
[フレーム]
[legend]
+ Collaboration diagram for path_fifot:
[フレーム]
[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< 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

FIFO save queue: paths are resumed in the order that they were saved.

Definition at line 183 of file path_storage.h.

Member Function Documentation

◆  clear()

void path_fifot::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 79 of file path_storage.cpp.

◆  private_peek()

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

Implements path_storaget.

Definition at line 59 of file path_storage.cpp.

◆  private_pop()

void path_fifot::private_pop ( )
overrideprivatevirtual

Implements path_storaget.

Definition at line 69 of file path_storage.cpp.

◆  push()

void path_fifot::push ( const patht &  )
overridevirtual

Add a path to resume to the storage.

Implements path_storaget.

Definition at line 64 of file path_storage.cpp.

◆  size()

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

How many paths does this storage contain?

Implements path_storaget.

Definition at line 74 of file path_storage.cpp.

Member Data Documentation

◆  paths

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

Definition at line 191 of file path_storage.h.

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

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