Cannot handle size of types larger than Integer.MAX_VALUE
typedef __SIZE_TYPE__ Size_t;
#define bufsize ((1L << (8 * sizeof(Size_t) - 2))-256)
struct huge_struct
{
short buf[bufsize];
int a;
int b;
int c;
int d;
};
union huge_union
{
int a;
char buf[bufsize];
};
Size_t union_size()
{
return sizeof(union huge_union);
}
Size_t struct_size()
{
return sizeof(struct huge_struct);
}
int main()
{
/* Check the exact sizeof value. bufsize is aligned on 256b. */
if (union_size() != sizeof(char) * bufsize)
{ERROR:goto ERROR;}
if (struct_size() != sizeof(short) * bufsize + 4*sizeof(int))
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
Edited by Philipp Wendler