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

Recursion-set entry owner class. More...

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

Public Member Functions

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

Private Attributes

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

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_set set 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
entry entry 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:

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