-
Notifications
You must be signed in to change notification settings - Fork 159
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
Bogus error: unreachable: code is dead #80
Comments
Instead, a valid warning would be |
Hi @yurivict, You are right. Since ikos doesn't have the code of the functions I agree that in this case we should emit 2 more warnings. I will make a patch soon, ikos should emit something like:
The other warnings are also related to this. IKOS doesn't know Even after fixing these, we will still get |
I agree. You should teach him all simple library functions. |
Using 79942e6, I'm now getting:
It is now more clear that the implementation of IKOS still doesn't know about libc functions |
I tried ikos on one file from the FreeBSD source tree,
hexdump.c
:It printed this warning, among others:
This code is obviously reachable. This
for
loop might never execute, iffshead
is left to beNULL
, butikos
has no way of knowing this without seeingnewsyntax
oroldsyntax
functions sincefshead
isn't static.It also printed:
The type of
argv
is defined, and these statements seem to be valid.ikos-2.1.52
FreeBSD 11.2 amd64
The text was updated successfully, but these errors were encountered: