Pointer arithmetic handled differently than array subscripts in predicate analysis
int main()
{
int tmp[2];
int *p, *q;
p = tmp;
q = p + 1;
*q = 0;
tmp[1] = 39;
if (*q != 39)
{ERROR:goto ERROR;}
return 0;
}
In this case, the ERROR label is infeasible, which is confirmed by compiling with gcc and clang, while CPAchecker gives the FALSE result which means ERROR label is feasible.
Command: ~/cpachecker/scripts/cpa.sh -config ~/cpachecker/config/predicateAnalysis.properties -skipRecursion -64 -preprocess -setprop cpa.predicate.handleStringLiteralInitializers=true <file_name.h>
OS:Ubuntu 14.04
Revision: 28771
I guess it is related to array pointer aliasing.
Edited by Philipp Wendler