Open JonasKlamroth opened 3 years ago
Paging @tautschnig @kroening who might know more about this.
This is a known issue, and there are currently no concrete plans to fix this. In the meanwhile, you can work around it by encoding the desired behavior yourself, e.g.
import org.cprover.CProver;
public class Test {
private void entryPoint(Object o1, Object o2, boolean equal) {
if (equal) {
o2 = o1;
}
test(o1, o2);
}
private void test(Object o1, Object o2) {
CProver.assume(o1 == o2 && o1 != null);
assert false;
}
}
and then run jbmc Test.entryPoint
.
Thank you for the workaround.
I thought about trying to implement this myself. Can you estimate the complexity of this endeavor? If you think it can be done with reasonable effort: Can you point me to a good place to start?
Complexity : Assuming you have a reasonable level of familiarity with the code / this kind of tool then the changes are not actually that difficult in this case but the general case is probably a bit harder. Configuring it could be a little tricky.
Plan of attack...
export CXXFLAGS="-O0 -g"; export LINKFLAGS=-rdynamic;
is your friend. So is rr
.jbmc
as well.--show-goto-functions
to show you the calling context that is auto-generated. This should give you a way of seeing what the effect of your changes are.--show-goto-functions
to look at the differences between the two.--show-goto-functions
HTH
Thank you. I will take a look at it.
JBMC version: 5.32.1 (cbmc-5.32.1-10-gb84b37dea) Operating system: Ubuntu 20.04.2 LTS Exact command line resulting in the issue: ./jbmc Test --function Test.test What behaviour did you expect: Verification should fail because of the "assert false" What happened instead: Verification was sucessful
Above information are the result given the following content of Test.java:
I assume this is the result of non deterministic objects being treated as new objects with nondeterministic fields, which is implicitly makes the assumption that those objects cannot alias. Is there a way to prevent this behavior? Are there plans to implement this in the future?