CBMC
|
Enumerators that enumerates expressions in the union of enumerated expressions of sub-enumerators. More...
#include <expr_enumerator.h>
Public Member Functions | |
alternatives_enumeratort (const enumeratorst &enumerators, const namespacet &ns) | |
expr_sett | enumerate (const std::size_t size) const override |
Public Member Functions inherited from enumerator_baset | |
enumerator_baset (const namespacet &ns) | |
enumerator_baset (const enumerator_baset &other)=delete | |
enumerator_baset & | operator= (const enumerator_baset &other)=delete |
virtual | ~enumerator_baset ()=default |
Protected Attributes | |
const enumeratorst | sub_enumerators |
Protected Attributes inherited from enumerator_baset | |
const namespacet & | ns |
Enumerators that enumerates expressions in the union of enumerated expressions of sub-enumerators.
For sub enumerator E_1 | E_2 | ... | E_n, an alternatives enumerator enumerates e in one of E_i.enumerate(size)
.
Definition at line 283 of file expr_enumerator.h.
|
inline |
Definition at line 286 of file expr_enumerator.h.
|
overridevirtual |
Implements enumerator_baset.
Definition at line 405 of file expr_enumerator.cpp.
|
protected |
Definition at line 296 of file expr_enumerator.h.