The list of code patterns where verification does not work well
Opened this issue · 1 comments
zpzigi754 commented
The below will summarize the code patterns which are not supported by formal verification tools.
[KLEE]
lazy_static: causes abort in klee processing
extern "C" fn: causes abort in klee processing
usize::from_le_bytes: causes abort in klee processing
fn name(self): causes abort in klee processing
...
bokdeuk-jeong commented
I understand why we need pr252. However, I still don't understand why 'fn name(self)' results aborts while processing Islet with klee. Could you explain more about this?