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


_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to