Skip to content

Commit 614eaef

Browse files
committed
Change pointer type in 7690 regression test and remove winbug designation.
1 parent 640c0be commit 614eaef

File tree

2 files changed

+3
-6
lines changed

2 files changed

+3
-6
lines changed

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ void smap_init(smap_t *smap, size_t k) {
2323

2424
void *smap_get(smap_t *smap, void *ptr) {
2525
size_t id = __CPROVER_POINTER_OBJECT(ptr);
26-
void *sptr = smap->ptrs[id];
26+
char *sptr = smap->ptrs[id];
2727
if (!sptr) {
2828
sptr = __CPROVER_allocate(smap->k * __CPROVER_OBJECT_SIZE(ptr), 1);
2929
smap->ptrs[id] = sptr;
Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
CORE smt-backend winbug
1+
CORE smt-backend
22
singleton_interval_in_assume_7690.c
33
--pointer-check
4-
^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed long int\)stk-\>top\]: SUCCESS$
4+
^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed (long|long long) int\)stk-\>top\]: SUCCESS$
55
^VERIFICATION SUCCESSFUL$
66
^EXIT=0$
77
^SIGNAL=0$
@@ -12,6 +12,3 @@ https://github.com/diffblue/cbmc/pull/7761 this would fail in
1212
the (old) SMT backend in /src/solvers/smt2, because some constraints
1313
would not be propagated correctly, leaving the value of `stk_size`
1414
in `stk_new` as nondet.
15-
16-
This fails on Windows VS2019 with `pointer arithmetic with unknown object size`,
17-
hence marked `winbug` to skip running on that system.

0 commit comments

Comments
 (0)