Skip to content

Commit 4fbe479

Browse files
committed
Add tests covering error handling
None of our existing tests covers the failure paths of type checking saturating arithmetic and character literal conversion, respectively.
1 parent 86284ae commit 4fbe479

File tree

5 files changed

+41
-0
lines changed

5 files changed

+41
-0
lines changed
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
unsupported.c
3+
-DWIDE
4+
wide literals with 5 characters are not supported$
5+
^EXIT=70$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
^Invariant check failed$
10+
--
11+
Test to confirm that an actionable error message is provided.
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
#ifndef WIDE
4+
'abcde';
5+
#else
6+
(void)L'abcde';
7+
#endif
8+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
unsupported.c
3+
4+
literals with 5 characters are not supported$
5+
^EXIT=70$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
^Invariant check failed$
10+
--
11+
Test to confirm that an actionable error message is provided.
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int main()
2+
{
3+
__CPROVER_saturating_minus(1);
4+
}
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
typeconflict.c
3+
file typeconflict.c line 3 function main: __CPROVER_saturating_minus takes exactly two arguments, but 1 were provided
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring

0 commit comments

Comments
 (0)