Skip to content

Commit 23d10ec

Browse files
committed
add two failing tests for preincrement on _Bool
This adds two tests that expose bugs when doing preincrement on C99 _Bool.
1 parent 123e02a commit 23d10ec

File tree

4 files changed

+46
-0
lines changed

4 files changed

+46
-0
lines changed

regression/cbmc/Bool/bool6.c

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int main()
2+
{
3+
_Bool u = 1;
4+
_Bool *p = &u;
5+
6+
// combination of _Bool, dereference, and pre-increment side-effect
7+
if(++(*p) != 1)
8+
__CPROVER_assert(0, "");
9+
10+
// combination of _Bool, dereference, and compound assignment side-effect
11+
if(((*p) += 1) != 1)
12+
__CPROVER_assert(0, "");
13+
14+
// combination of _Bool, dereference, and assignment side-effect
15+
if(((*p) = 1) != 1)
16+
__CPROVER_assert(0, "");
17+
18+
__CPROVER_assert(*p == 1, "");
19+
}

regression/cbmc/Bool/bool6.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
bool6.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

regression/cbmc/Bool/bool7.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
_Bool u = 1;
6+
7+
// assert the type of side effects on _Bool
8+
assert(sizeof(++u) == sizeof(_Bool));
9+
assert(sizeof(u += 1) == sizeof(_Bool));
10+
assert(sizeof(u = 1) == sizeof(_Bool));
11+
}

regression/cbmc/Bool/bool7.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
bool7.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)