Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

The list of code patterns where verification does not work well #247

Open
zpzigi754 opened this issue Dec 5, 2023 · 1 comment
Open

The list of code patterns where verification does not work well #247

zpzigi754 opened this issue Dec 5, 2023 · 1 comment

Comments

@zpzigi754
Copy link
Collaborator

zpzigi754 commented Dec 5, 2023 •
edited
Loading

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
...
zpzigi754 added a commit to zpzigi754/islet that referenced this issue Dec 15, 2023
@zpzigi754
klee: Fix self's usage where its reference is implied
f7d560d 
This is required for KLEE integration. Before this change, KLEE
has aborted on compiling the previous code.

Relates to islet-project#247
@zpzigi754 zpzigi754 mentioned this issue Dec 15, 2023
Merged
zpzigi754 added a commit that referenced this issue Dec 18, 2023
@zpzigi754
klee: Fix self's usage where its reference is implied
0cbf094 
This is required for KLEE integration. Before this change, KLEE
has aborted on compiling the previous code.

Relates to #247
@bokdeuk-jeong
Copy link
Collaborator

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@zpzigi754 @bokdeuk-jeong