Write through aliased pointer not detected as relevant in predicate analysis
int b[32];
int *r = b;
int
main(void)
{
r[2] = 77;
if (b[2] != 77)
{ERROR:goto ERROR;}
return 0;
}
int a3[3];
void f(int *a)
{
a[1] = 42;
}
int
main ()
{
f(a3);
if (a3[1] != 42)
{ERROR:goto ERROR;}
return 0;
}
In both cases, 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
CPAchecker gives the expected result with command:
~/cpachecker/scripts/cpa.sh -config ~/cpachecker/config/predicateAnalysis.properties -skipRecursion -64 -preprocess -setprop cpa.predicate.handleStringLiteralInitializers=true -setprop cpa.predicate.ignoreIrrelevantVariables=false <file_name.h>
Edited by Philipp Wendler