'format_classpath.sh' is used in regression tests that make use of the
'classpath' option. This script is needed to deal with the fact that
classpath syntex is OS-dependent.
The java concurrency regression tests make heavy use of this option as
such this commit moves 'format_classpath.sh' to
'scripts/format_classpath.sh'.
Furthermore, this commit makes a very small change to 'appveyor.yml'
that enables existing java concurrency regression tests to run on
Windows.
Also fixes a number of shortcomings of the earlier approach as far as CMake is
concerned:
- Adds --dirty to the git command line (as is done for Makefiles).
- Does not require a rebuild when there are no changes to the version string.
- CBMC release number updates will be reflected and trigger a rebuild (even when
no other changes have taken place).
This uses the output of `git-describe --tags --always --dirty` to create a UID
for binaries. This includes last tag, number of commits after last tag,
shortened SHA1 checksum and optional dirty flag for uncommited changes. In case
of tagged commit, only the tag name is used.
This will allow for loading for example, all constructors or all methods
called getSomething.
Tests using this require minor modifications when they have specified
the descriptor as the brackets must be escaped for the regex. However,
the new code handles the case where no descriptor is provided (in which
case it will match all overloads) and the case where no java:: prefix
has been provided, leaving similar behaviour.
Correcting documentation for the extra entry points
This is less agressive than the original solution of not instantating
abstract types in ci_lazy_methods at all. This is done to minimize the
changes this PR introduces.
Use gather all fields when setting up the return of an opaque method
This can be considered an input to the function under test, so therefore
we need to set it up in the same way.
If the 'java-threading' option is specified this commit prevents symex
from throwing an exception when it encounters pointers that are shared
across threads. This is unsound but given that pointers are ubiquitous
in java this check must be disabled (until the concurrency encoding is
fixed).
Assertions in Java are "throw a;" statements where
a is of type java.lang.AssertionError (an exception,
or Throwable, to be precise). Sometimes we want to
translate it into an ASSERT instruction in the goto
program. Special-casing in order to handle that
was scattered across multiple classes. In this commit
we special-case it only once in the Java frontend
and translate it into assert(false); assume(false);
which is then correctly handled by later stages of the
translation.
That's the default behaviour because an escaping exception
makes the JVM abort. The user can override this behaviour
using the --disable-uncaught-exception-check option.
Kurt Degiorgio