Skip to content

Commit 2d00944

Browse files
Add test for shadow memory of __errno
We must be able to attach shadow memory to the memory returned by __errno().
1 parent 93fb568 commit 2d00944

File tree

2 files changed

+23
-0
lines changed

2 files changed

+23
-0
lines changed
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
#include <errno.h>
3+
4+
int main()
5+
{
6+
__CPROVER_field_decl_local("field1", (_Bool)0);
7+
__CPROVER_field_decl_global("field1", (_Bool)0);
8+
9+
int *error = __errno();
10+
11+
assert(__CPROVER_get_field(error, "field1") == 0);
12+
13+
__CPROVER_set_field(error, "field1", 1);
14+
assert(__CPROVER_get_field(error, "field1") == 1);
15+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)