The list of code patterns where verification does not work well

[zpzigi754]

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]

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?