[klee-dev] The false positives incurred when --max-sym-array-size flag is used

[Peng Li]

Hi All

When I running KLEE, I sometimes encountered the warning exposed by KLEE:

KLEE: WARNING: flushing 16384 bytes on read, may be slow and/or crash: 
MO57488[16384] allocated at cudaMalloc():  %call = tail call noalias i8* 
@malloc(i64 %size) nounwind, !dbg !1052

And there will happen segment fault at some steps of execution, then I 
have to use --max-sym-array-size flag to avoid the
warning and execution abortion, however, the false positives will be 
incurred.

Do you have any idea on why this happens?

Regards
Peng