Skip to content

Commit 832a800

Browse files
author
Enrico Steffinlongo
authored
Merge pull request #7879 from esteffin/esteffin/fix-shadow-memory-regressions
Fix many shadow memory regressions
2 parents 2daecc3 + 6f974d7 commit 832a800

File tree

9 files changed

+23
-17
lines changed

9 files changed

+23
-17
lines changed
Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--unwind 11
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
7-
^Generated 11 VCC\(s\), 0 remaining after simplification$
7+
^Generated \d+ VCC\(s\), 0 remaining after simplification$
88
--
99
^warning: ignoring

regression/cbmc-shadow-memory/global1/main.c

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ void dynamically_allocated_structs()
155155
assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 2);
156156
assert(__CPROVER_get_field(&(p->B1[2]), "field1") == 0);
157157

158-
q = &(p->B1[2]);
158+
int *q = &(p->B1[2]);
159159
assert(__CPROVER_get_field(q, "field1") == 0);
160160
__CPROVER_set_field(q, "field1", 7);
161161
assert(__CPROVER_get_field(q, "field1") == 7);
@@ -187,7 +187,7 @@ void arrays_of_structs_and_pointers_into_them()
187187
assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 3);
188188
assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
189189

190-
q = &(n[1].x1);
190+
int *q = &(n[1].x1);
191191
assert(__CPROVER_get_field(q, "field1") == 1);
192192
__CPROVER_set_field(q, "field1", 5);
193193
assert(__CPROVER_get_field(q, "field1") == 5);
@@ -197,6 +197,8 @@ void arrays_of_structs_and_pointers_into_them()
197197
__CPROVER_set_field(q, "field2", 6);
198198
assert(__CPROVER_get_field(q, "field2") == 6);
199199

200+
int k;
201+
__CPROVER_assume(0 <= k && k < 3);
200202
int x;
201203
__CPROVER_assume(0 <= x && x < 3);
202204
__CPROVER_set_field(&(n[k].B1[x]), "field1", 46);
@@ -226,7 +228,7 @@ void dynamically_allocated_arrays_of_structs()
226228
assert(__CPROVER_get_field(&(u[1].B1[1]), "field2") == 3);
227229
assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
228230

229-
q = &(u[1].x1);
231+
int *q = &(u[1].x1);
230232
assert(__CPROVER_get_field(q, "field1") == 1);
231233
__CPROVER_set_field(q, "field1", 5);
232234
assert(__CPROVER_get_field(q, "field1") == 5);
@@ -236,6 +238,8 @@ void dynamically_allocated_arrays_of_structs()
236238
__CPROVER_set_field(q, "field2", 6);
237239
assert(__CPROVER_get_field(q, "field2") == 6);
238240

241+
int k;
242+
__CPROVER_assume(0 <= k && k < 3);
239243
int t;
240244
__CPROVER_assume(0 <= t && t < 3);
241245
__CPROVER_set_field(&(u[k].B1[t]), "field1", 46);

regression/cbmc-shadow-memory/global1/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$

regression/cbmc-shadow-memory/local1/main.c

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ void arrays_and_pointers_into_arrays()
5353
{
5454
int A[5];
5555

56-
z = &(A[4]);
56+
int *z = &(A[4]);
5757

5858
assert(__CPROVER_get_field(z, "field1") == 0);
5959
assert(__CPROVER_get_field(z, "field2") == 0);
@@ -111,7 +111,7 @@ void structs_and_pointers_into_structs()
111111
__CPROVER_set_field(&(m.B1[j]), "field1", 44);
112112
assert(__CPROVER_get_field(&(m.B1[j]), "field1") == 44);
113113

114-
z = &(m.B1[j]);
114+
int *z = &(m.B1[j]);
115115
__CPROVER_set_field(z, "field1", 45);
116116
assert(__CPROVER_get_field(z, "field1") == 45);
117117
}
@@ -123,7 +123,7 @@ void arrays_of_structs_and_pointers_into_them()
123123
assert(__CPROVER_get_field(&(n[1].x1), "field1") == 0);
124124
assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 0);
125125

126-
p = &(n[2]);
126+
struct STRUCTNAME *p = &(n[2]);
127127

128128
__CPROVER_set_field(&(n[1].x1), "field1", 1);
129129
__CPROVER_set_field(&(p->x1), "field1", 2);
@@ -135,7 +135,7 @@ void arrays_of_structs_and_pointers_into_them()
135135
assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 3);
136136
assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
137137

138-
q = &(n[1].x1);
138+
int *q = &(n[1].x1);
139139
assert(__CPROVER_get_field(q, "field1") == 1);
140140
__CPROVER_set_field(q, "field1", 5);
141141
assert(__CPROVER_get_field(q, "field1") == 5);
@@ -147,10 +147,12 @@ void arrays_of_structs_and_pointers_into_them()
147147

148148
int k;
149149
__CPROVER_assume(0 <= k && k < 3);
150+
int j;
151+
__CPROVER_assume(0 <= j && j < 3);
150152
__CPROVER_set_field(&(n[k].B1[j]), "field1", 46);
151153
assert(__CPROVER_get_field(&(n[k].B1[j]), "field1") == 46);
152154

153-
z = &(n[k].B1[j]);
155+
int *z = &(n[k].B1[j]);
154156
__CPROVER_set_field(z, "field1", 47);
155157
assert(__CPROVER_get_field(z, "field1") == 47);
156158
}

regression/cbmc-shadow-memory/local1/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$

regression/cbmc-shadow-memory/param1/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ void f_int_local(int rec, int value)
103103

104104
int main()
105105
{
106-
__CPROVER_field_decl_local("field1", (char)0);
106+
__CPROVER_field_decl_local("field1", (unsigned char)0);
107107
int x;
108108
__CPROVER_set_field(&x, "field1", 255);
109109
f_int_val(x);

regression/cbmc-shadow-memory/param1/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$

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)