Skip to content

Commit

Permalink
Re-add pointer dec tests
Browse files Browse the repository at this point in the history
  • Loading branch information
dc-mak committed Aug 13, 2024
1 parent 8e2f528 commit 9b52832
Show file tree
Hide file tree
Showing 5 changed files with 76 additions and 0 deletions.
20 changes: 20 additions & 0 deletions src/example-archive/c-testsuite/broken/error-proof/00073.err1.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
/*
cn: internal error, uncaught exception:
Failure("todo")
*/
// Cause: `-=` assignment operator

int
main()
{
int arr[2];
int *p;

p = &arr[1];
p -= 1;
*p = 123;

if(arr[0] != 123)
return 1;
return 0;
}
35 changes: 35 additions & 0 deletions src/example-archive/c-testsuite/working/00032.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
// Crash: caused by pointer decrement

int
main()
/*@ ensures return == 0i32; @*/
{
int arr[2];
int *p;

/*@ extract Block<int>, 0u64; @*/
arr[0] = 2;
/*@ extract Block<int>, 1u64; @*/
arr[1] = 3;
p = &arr[0];
if(*(p++) != 2)
return 1;
if(*(p++) != 3)
return 2;

p = &arr[1];
if(*(p--) != 3)
return 1;
if(*(p--) != 2)
return 2;

p = &arr[0];
if(*(++p) != 3)
return 1;

p = &arr[1];
if(*(--p) != 2) // <-- cause of the crash
return 1;

return 0;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
// Crash

void
pointerdec_crash_3()
{
int arr[2];
int *p = &arr[1];
*(--p);
}
5 changes: 5 additions & 0 deletions src/example-archive/simple-examples/working/pointer_dec1.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
int a;
void b() {
int *c = &a;
c -= 1;
}
7 changes: 7 additions & 0 deletions src/example-archive/simple-examples/working/pointer_dec2.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
// Derived from src/example-archive/c-testsuite/broken/error-proof/00032.err1.c

int a;
void b() {
int *c = &a;
--c;
}

0 comments on commit 9b52832

Please sign in to comment.