Always check Java pointers for null before deref #737
Conversation
smowton
force-pushed
the
java_null_checks
branch
from
5dada64 to
b993b26
Compare
src/analyses/goto_check.cpp
Outdated
| goto_check.goto_check(it->second); | ||
| const symbolt *sym; | ||
| irep_idt mode; | ||
| if(!ns.lookup(it->first, sym)) |
There was a problem hiding this comment.
Shouldn't it be an invariant that the symbol exists? I think it should be safe to use
irep_idt mode=ns.lookup(it->first).mode;
?
There was a problem hiding this comment.
Unsure, hence being careful.
There was a problem hiding this comment.
I'd go all-in and wait for bug reports (or failing regression tests).
There was a problem hiding this comment.
Ok will change this shortly
| { | ||
| if(!enable_pointer_check) | ||
| if(mode!=ID_java && !enable_pointer_check) |
There was a problem hiding this comment.
So we would always be doing this for mode==ID_java, whether it's enabled or not!?
There was a problem hiding this comment.
Yes. Check-deref'd-pointer-not-null is mandatory for Java. Explicit enable is only then meaningful for C/C++/etc.
There was a problem hiding this comment.
But we should then be generating an exception, not an assertion, shouldn't we?
There was a problem hiding this comment.
Ideally yes. However this matches current Java front-end behaviour for out of bounds array access and similar. I think we should support this simple model and then perhaps in the future add support for a "full fidelity" model where we support catching NPE, AOOBE and so on.
There was a problem hiding this comment.
Ok; I'd thus suggestion that the help output for --pointer-check be amended to say "C/C++ only".
This also improves goto-check's resolution for finding symbol modes by finding the function in the symbol table and parameterising from above.
smowton
force-pushed
the
java_null_checks
branch
from
b993b26 to
f15ebdf
Compare
They required "1 of N successful" reports, where N is changed by the addition of new assertions.
This is effectively always enabled for Java programs now. For others this is still optional.
smowton
force-pushed
the
java_null_checks
branch
from
9cef302 to
f9cd371
Compare
This also improves goto-check's resolution for finding symbol modes by finding the function in the symbol table and parameterising from above.
I wrote this because the test generator was producing strange results due to missing null checks. Before the test generator became a separate module it twiddled the command-line options to add
pointer-check; however I think doing it this way is better, as it is never semantically sane to analyse Java-but-null-pointers-are-wild.