Skip to content

Commit a02416f

Browse files
author
Enrico Steffinlongo
committed
Add regression tests for UNREACHABLE_BECAUSE
1 parent b6ba164 commit a02416f

File tree

2 files changed

+14
-0
lines changed

2 files changed

+14
-0
lines changed

regression/invariants/driver.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,8 @@ int main(int argc, char** argv)
112112
UNREACHABLE_STRUCTURED(structured_error_testt, 1, "Structured error"); // NOLINT
113113
else if(arg=="unreachable-string")
114114
UNREACHABLE;
115+
else if(arg == "unreachable-because")
116+
UNREACHABLE_BECAUSE("Unreachable with explanation text");
115117
else if(arg=="data-invariant-structured")
116118
DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
117119
else if(arg=="data-invariant-string")
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
dummy_parameter.c
3+
unreachable-because
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
Unreachable with explanation text
8+
Invariant check failed
9+
^(Backtrace)|(Backtraces not supported)$
10+
--
11+
^warning: ignoring
12+
^VERIFICATION SUCCESSFUL$

0 commit comments

Comments
 (0)