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

[Cristian Cadar]

Hi Peng,

Post by Peng Li
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.

Does KLEE report a bug which is not real? If so, please fill a bug
report on GitHub.

Thanks,
Cristian