CBMC
recursion_set_entryt Class Reference

Recursion-set entry owner class. More...

+ Collaboration diagram for recursion_set_entryt:

Public Member Functions

 recursion_set_entryt (std::unordered_set< irep_idt > &_recursion_set)
 Initialize a recursion-set entry owner operating on a given set. More...
 
 ~recursion_set_entryt ()
 Removes erase_entry (if set) from the controlled set. More...
 
 recursion_set_entryt (const recursion_set_entryt &)=delete
 
recursion_set_entrytoperator= (const recursion_set_entryt &)=delete
 
bool insert_entry (const irep_idt &entry)
 Try to add an entry to the controlled set. More...
 

Private Attributes

std::unordered_set< irep_idt > & recursion_set
 Recursion set to modify. More...
 
irep_idt erase_entry
 Entry to erase on destruction, if non-empty. More...
 

Detailed Description

Recursion-set entry owner class.

If a recursion-set entry is added in a particular scope, ensures that it is erased on leaving that scope.

Definition at line 266 of file java_object_factory.cpp.

Constructor & Destructor Documentation

◆ recursion_set_entryt() [1/2]

recursion_set_entryt::recursion_set_entryt ( std::unordered_set< irep_idt > &  _recursion_set)
inlineexplicit

Initialize a recursion-set entry owner operating on a given set.

Initially it does not own any set entry.

Parameters
_recursion_setset to operate on.

Definition at line 277 of file java_object_factory.cpp.

◆ ~recursion_set_entryt()

recursion_set_entryt::~recursion_set_entryt ( )
inline

Removes erase_entry (if set) from the controlled set.

Definition at line 282 of file java_object_factory.cpp.

◆ recursion_set_entryt() [2/2]

recursion_set_entryt::recursion_set_entryt ( const recursion_set_entryt )
delete

Member Function Documentation

◆ insert_entry()

bool recursion_set_entryt::insert_entry ( const irep_idt entry)
inline

Try to add an entry to the controlled set.

If it is added, own that entry and erase it on destruction; otherwise do nothing.

Parameters
entryentry to add
Returns
true if added to the set (and therefore owned by this object)

Definition at line 295 of file java_object_factory.cpp.

◆ operator=()

recursion_set_entryt& recursion_set_entryt::operator= ( const recursion_set_entryt )
delete

Member Data Documentation

◆ erase_entry

irep_idt recursion_set_entryt::erase_entry
private

Entry to erase on destruction, if non-empty.

Definition at line 271 of file java_object_factory.cpp.

◆ recursion_set

std::unordered_set<irep_idt>& recursion_set_entryt::recursion_set
private

Recursion set to modify.

Definition at line 269 of file java_object_factory.cpp.


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