-
Notifications
You must be signed in to change notification settings - Fork 86
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.
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
Point-to-analysis fail if an instance does not have a body #3447
Comments
That's weird. It seems like the error is caused by following this kani/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs Lines 208 to 210 in e6f8a62
However, we later fail to obtain the actual body for the intrinsic here: kani/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs Lines 446 to 450 in e6f8a62
I think we should be getting the body via |
I believe the problem here is that StableMIR already includes both checks. |
Thanks! That's good to know. It turned out I only had to add support for 3 intrinsics to get rid of |
Initially, points-to analysis tried to determine the body of an intrinsic (if it was available) to avoid enumerating them all. However, it turned out this logic was faulty, and the analysis attempted to query the body for intrinsics that didn't have it and ICEd. I added a couple of missing intrinsics, which had a side benefit of removing some duplicate assertion failures. Resolves #3447 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
I tried this code:
using the following command line invocation:
with Kani version:
I expected to see this happen: Verification succeeds
Instead, this happened: Kani crashes
The text was updated successfully, but these errors were encountered: