Template Class WithGroup

• Defined in File with_context.h

Class Documentation

template<typename ContextType>
class WithGroup

A group of RAII contexts managed together.

Allows dynamically emplacing multiple context objects that are all exited (in reverse order) when the group is destroyed. ContextType must declare friend class With<ContextType> and provide EnterWithScope() / ExitWithScope() methods.

WithGroup<sym::AllowUIntAsIndex> group;
group.Emplace();  // enters the first no-overflow assumption scope
group.Emplace();  // enters a nested scope
// Destruction exits the scopes in reverse order.

Template Parameters:

ContextType – The context type with EnterWithScope/ExitWithScope.

Public Functions

WithGroup() = default

WithGroup(WithGroup&&) = default

WithGroup &operator=(WithGroup&&) = default

WithGroup(const WithGroup&) = delete

WithGroup &operator=(const WithGroup&) = delete

template<typename ...Args>
inline void Emplace(Args&&... args)

Construct a context and enter its scope.

Parameters:

args – Arguments forwarded to ContextType constructor.

inline size_t size() const

Number of active contexts in this group.

inline ~WithGroup()

Destructor — exits all contexts in reverse order.

On normal exit: if any ExitWithScope throws, the remaining contexts are still cleaned up, then the first exception is re-thrown.

During stack unwinding: all exceptions are swallowed to avoid std::terminate.