Please document use of assumptions, non-determinism in Java

[tautschnig]

As the regression tests don't seem to provide a lot of insight, it would be great to have some documentation that explains how to use the fundamental modelling constructs with Java. While assert is fine, non-determinism seems to be expressible using (not internally defined) Java library functions. That still leaves assumptions, which I'm not sure how to deal with.

Thanks,
Michael

[thomasspriggs]

For jbmc assumptions can be added to user code, by adding calls to the static method assume of the dummy CProver class in the org.cprover package. This method takes a single boolean argument which is the condition to be assumed.

For the user code calling the assume method to compile with the java compiler, a version of this CProver class is required, but its contents is not relevant to our analysis. For an example of the dummy class see - jbmc/regression/jbmc-strings/cprover/CProver.java.

The assumptions are then implemented inside jbmc based on replacing calls to the assume method with instances of code_assumet, which is why the contents of the CProver matter only to the Java compiler. The implementation of this replacement can be found here

cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Line 1323 in b345e2a

bytecode == BC_invokestatic && id2string(arg0.get(ID_identifier)) ==

It would be better if there was a standardised version of the CProver class available, instead of being defined adhoc in regression tests; to go with the relevant documentation. I am assuming that this hasn't been done due to this functionality being added with the intention of making it easier to write regression tests, rather than as a user facing feature.

[peterschrammel]

The CProver Java API is available here: https://mvnrepository.com/artifact/org.cprover.util/cprover-api/1.0.0
You add this dependency to your project so that you can compile your code when you use CProver.assume, CProver.nondetInt, etc.

[thomasspriggs]

Nice. I'd forgotten that we had published this to Maven. It could still do with being better documented in doc/cprover-manual/jbmc-user-manual.md though. There is a single sentence in there about the package, but not where to find it, or what utilities are available.