Description
In the sv-benchmarks run of #1552 with vojdani privatization I noticed a particularly odd spurious overflow warning:
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack-pthread.i:742:3-742:16)
The line in question is
r = push(arg);where both r and arg are int and so are the types for push.
Tracing revealed that these overflow warnings are emitted during smart_join of the partitioned array domain when it evaluates expressions. The weird location is because this isn't happening during a transfer function, but it's a join on an global unknown.
Although the problem only revealed itself with the vojdani privatization from #1552, the underlying problem is more general. It seems that partitioned arrays are side-effected to globals while still referring to local variables:
%%% priv: sideg memory (partitioned array:Array: Array (part. by newTop + 1): (Uninitialized -- 0 -- 0), IntDomLifter(intdomtuple):65)
A subsequent join in the solver then leads to the array domain trying to evaluate newTop + 1, where newTop cannot have any value (so it's VD.bot, then turned into VD.top). The overflow warning comes from trying to add to the supertop.
We probably should suppress overflow warnings from these partitioned array expression evaluations, but that's just a coverup: such expressions shouldn't be side-effected in the first place.