Corner case in pointer-overflow-check #6631
Description
CBMC version: 5.48
Operating system: OSX
Exact command line resulting in the issue: cbmc --pointer-overflow-check test.c
What behaviour did you expect: Overflow detected
What happened instead:
╰─$ cbmc --pointer-overflow-check test.c
CBMC version 5.48.0 (cbmc-5.48.0) 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00214797s
size of program expression: 45 steps
simple slicing removed 0 assignments
Generated 2 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 2.109e-05s
** Results:
test.c function main
[main.pointer_arithmetic.1] line 7 pointer arithmetic: dead object in p + 9223372036854775807l: SUCCESS
[main.pointer_arithmetic.2] line 7 pointer arithmetic: pointer outside object bounds in p + 9223372036854775807l: SUCCESS
** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL
#include <limits.h>
#include <stdint.h>
int main() {
int i[5];
int*p = &i[1]; // Spurious success. Change to any other offset to get the expected fail
int*q = p + SSIZE_MAX;
}