diff --git a/regression/cbmc/pointer-overflow2/main.c b/regression/cbmc/pointer-overflow2/main.c new file mode 100644 index 00000000000..e73ba1eb115 --- /dev/null +++ b/regression/cbmc/pointer-overflow2/main.c @@ -0,0 +1,10 @@ +#include + +void main() +{ + char *p = (char *)10; + p -= 1; + p += 1; + p += -1; // spurious pointer overflow report + p -= -1; // spurious pointer overflow report +} diff --git a/regression/cbmc/pointer-overflow2/test.desc b/regression/cbmc/pointer-overflow2/test.desc new file mode 100644 index 00000000000..0cd1d164728 --- /dev/null +++ b/regression/cbmc/pointer-overflow2/test.desc @@ -0,0 +1,11 @@ +KNOWNBUG +main.c +--pointer-overflow-check +^EXIT=0$ +^SIGNAL=0$ +\[main.overflow.1\] line \d+ pointer arithmetic overflow on - in p - \(signed long int\)1: SUCCESS +\[main.overflow.2\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long int\)1: SUCCESS +\[main.overflow.3\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long int\)-1: SUCCESS +\[main.overflow.4\] line \d+ pointer arithmetic overflow on - in p - \(signed long int\)-1: SUCCESS +-- +^warning: ignoring