This should be an output of the functions rather than an "info".
We make it so that assign_*_from_json functions have a return
type which reflects what the function does. That way we separate
the json to assignment conversion from the writting of code blocks,
which will ultimately allow us to rewrite references in the assignments.
This will be use in assign_from_json for json files in which the "@ref"
and "@id" entries are used, so that we can easily substitute code marked
by "@ref" by the code corresponding to the object marked by "@id".
This also move object_creation_referencet to the new header file since
it will be used there, and the allocate_array is now declared in the new
header and defined in the corresponding cpp file.
This means that generated error messages show what the particular
invariant failure actually generated was, instead of the catch framework
default of `{?}`.
`REQUIRE_THROWS_MATCHES` is the functionality built into the catch
framework for this purpose. Using it allows more concise specification
of the requirement.
When the array is not marked as nondet and is not a reference it can
directly be allocated with the right size, which will allow constant
propagation through arrays.
Depending on whether the array has deterministic length or not.
This will make it easier to allocate the array directly to the right
size in the deterministic case.
This makes it so that we only have one block.add(code_assumet(...))
instruction, it is thus easier to figure out what the assumption is
depending on the parameters.
This makes the assign_array_from_json a bit simpler.
This is an intermediary commit towards removing the optional argument
from assign_array_from_json.
These unit tests complement the regression tests in
jbmc/regression/jbmc/context-include-exclude
that were added in a previous commit to check for properties of excluded
methods. Some properties, like information about accessibility and final
and static status, is easier to check in unit-style tests.
The new overload allows specifying the command-line options to run jbmc
with. For example, we will be able to specify that --context-include
should be used.
The tests from the previous commit show that the right methods are
excluded.
The tests from this commit show that an excluded method has the right
properties: meta-information such as parameter types and identifiers
should be preserved, while the real method should not be loaded and a
stub-like "return nondet" body should be used instead.
The tests from this commit would not have passed without the fixes from
this PR.
The tests in this commit would have all passed without the previous
fixes already and are just added for completeness.
The tested prefixes are a prefix of a package and a prefix that does not
match anything on the classpath.
These lines appear in the output for methods whose body is empty/nil.
For excluded methods, we now have "return nondet" bodies as we do for
stubs, so the warnings are no longer printed.
If we are not using CI lazy methods here (as could happen after the
change from the previous commit that makes sure convert_single_method is
run for all methods), needed_lazy_methods is an empty optional and we
cannot access it.
The previous version would have not called convert_single_method on
excluded methods, meaning they would have missed some meta-information,
e.g. parameter identifiers.
There are three types of method symbols that we expect here:
1) symbols for regular methods, i.e. the bytecode of the method is
available and the method is in the supplied context
2) symbols for opaque methods, i.e. the bytecode of the method is not
available
3) symbols for excluded methods, i.e. the bytecode of the method is
available but the method is not in the supplied context
The previous check was correct for 1) and 2): we do not want to create
stub bodies ("return nondet") for regular methods but we do want to
create them for opaque methods.
The new check makes sure that stub bodies are also created for excluded
methods (3). Previously the value of those symbols was just left as nil,
meaning the (type of the) return value of the method was not constrained
in any way.
The previous check was right at the beginning of convert_single_method,
meaning that for an "excluded" method, we would have never entered
java_bytecode_convert_method, which assigns more than just the symbol
value (body of a method), e.g. parameter identifiers.
The only information that we want to omit for excluded methods is their
bodies / symbol values. This is why the new check is just before the
assignment of symbol values, making sure that parameter identifiers and
other meta-information of the method are correctly assigned for excluded
methods.
This means it can be used even in settings where a class hierarchy isn't
readily available. The class hierarchy was only being used to find
parents, which are easily available from the class type directly, so it
wasn't providing any benefit. (It would have been different if we needed
to find children.)
Romain Brenguier