Skip to content

Commit ef96d89

Browse files
author
Enrico Steffinlongo
committed
Fix shadow memory var-assign1 regression test
1 parent 80d5419 commit ef96d89

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

regression/cbmc-shadow-memory/var-assign1/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,9 @@
22

33
int main()
44
{
5-
__CPROVER_field_decl_local("field", (_Bool)0);
5+
__CPROVER_field_decl_local("field", (char)0);
66

7-
_Bool z;
7+
char z;
88
int x;
99
__CPROVER_set_field(&x, "field", z);
1010
assert(__CPROVER_get_field(&x, "field") == z);

regression/cbmc-shadow-memory/var-assign1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

0 commit comments

Comments
 (0)