diff --git a/src/example-archive/c-testsuite/broken/error-proof/00073.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00073.err1.c new file mode 100644 index 00000000..f32b1df7 --- /dev/null +++ b/src/example-archive/c-testsuite/broken/error-proof/00073.err1.c @@ -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; +} diff --git a/src/example-archive/c-testsuite/working/00032.c b/src/example-archive/c-testsuite/working/00032.c new file mode 100644 index 00000000..61fe917c --- /dev/null +++ b/src/example-archive/c-testsuite/working/00032.c @@ -0,0 +1,35 @@ +// Crash: caused by pointer decrement + +int +main() +/*@ ensures return == 0i32; @*/ +{ + int arr[2]; + int *p; + + /*@ extract Block, 0u64; @*/ + arr[0] = 2; + /*@ extract Block, 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; +} diff --git a/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c b/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c new file mode 100644 index 00000000..1b59c111 --- /dev/null +++ b/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c @@ -0,0 +1,9 @@ +// Crash + +void +pointerdec_crash_3() +{ + int arr[2]; + int *p = &arr[1]; + *(--p); +} diff --git a/src/example-archive/simple-examples/working/pointer_dec1.c b/src/example-archive/simple-examples/working/pointer_dec1.c new file mode 100644 index 00000000..a5d208da --- /dev/null +++ b/src/example-archive/simple-examples/working/pointer_dec1.c @@ -0,0 +1,5 @@ +int a; +void b() { + int *c = &a; + c -= 1; +} diff --git a/src/example-archive/simple-examples/working/pointer_dec2.c b/src/example-archive/simple-examples/working/pointer_dec2.c new file mode 100644 index 00000000..542a2108 --- /dev/null +++ b/src/example-archive/simple-examples/working/pointer_dec2.c @@ -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; +}