Skip to content

Commit a63ed68

Browse files
committed
Add UNIMPLEMENTED_FEATURE macro
So that messages can be included to describe exactly what it is which is unimplemented.
1 parent f82fea4 commit a63ed68

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/util/invariant.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -514,6 +514,9 @@ CBMC_NORETURN void report_invariant_failure(
514514
#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
515515
EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
516516

517+
#define UNIMPLEMENTED_FEATURE(FEATURE) \
518+
INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))
519+
517520
// Legacy annotations
518521

519522
// The following should not be used in new code and are only intended

0 commit comments

Comments
 (0)