Skip to content

Commit 3cf768b

Browse files
committed
array-cast adress equality: add check with addresses that should compare as unequal.
1 parent ea60c3d commit 3cf768b

1 file changed

Lines changed: 11 additions & 5 deletions

File tree

tests/regression/69-addresses/02-array-cast.c

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,16 +5,22 @@ int main() {
55
int a[10];
66
int *b = a;
77

8-
assert(a == b);
9-
assert(a + 4 == b + 4);
8+
__goblint_check(a == b);
9+
__goblint_check(a + 4 == b + 4);
1010

1111
char *b_char = (char*) a;
12-
assert((void*) a == (void*) b_char );
12+
__goblint_check((void*) a == (void*) b_char );
1313

14-
char* a_intoffset = a + 1;
15-
char* b_intoffset = b_char + sizeof(int);
14+
char* a_intoffset =(char*) (a + 1);
15+
char* b_intoffset = b_char + sizeof(int);
1616

1717
__goblint_check(a_intoffset == b_intoffset);
1818
__goblint_check((char*) (a + 1) == b_char + sizeof(int));
19+
20+
char* a_4intoffset = (char*) (a + 4);
21+
22+
__goblint_check(a_4intoffset == b_intoffset); // FAIL
23+
__goblint_check((char*) (a + 4) == b_char + sizeof(int)); // FAIL
24+
1925
return 0;
2026
}

0 commit comments

Comments
 (0)