CBMC
|
Recursion-set entry owner class. More...
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_entryt & | operator= (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... | |
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.
|
inlineexplicit |
Initialize a recursion-set entry owner operating on a given set.
Initially it does not own any set entry.
_recursion_set | set to operate on. |
Definition at line 277 of file java_object_factory.cpp.
|
inline |
Removes erase_entry (if set) from the controlled set.
Definition at line 282 of file java_object_factory.cpp.
|
delete |
|
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.
entry | entry to add |
Definition at line 295 of file java_object_factory.cpp.
|
delete |
|
private |
Entry to erase on destruction, if non-empty.
Definition at line 271 of file java_object_factory.cpp.
|
private |
Recursion set to modify.
Definition at line 269 of file java_object_factory.cpp.