-
Notifications
You must be signed in to change notification settings - Fork 273
[TG-4345] Parse thrown exceptions in java #2607
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[TG-4345] Parse thrown exceptions in java #2607
Conversation
jbmc/src/java_bytecode/java_types.h
Outdated
@@ -131,6 +131,16 @@ class java_class_typet:public class_typet | |||
return set(ID_outer_class, outer_class); | |||
} | |||
|
|||
const irep_idt get_super_class() const |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should be const irep_idt &
(same for outer_class above, actually)
jbmc/src/java_bytecode/java_types.h
Outdated
return get(ID_super_class); | ||
} | ||
|
||
void set_super_class(irep_idt super_class) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
const irep_idt &
method.exception_table[e].start_pc=start_pc; | ||
method.exception_table[e].end_pc=end_pc; | ||
method.exception_table[e].handler_pc=handler_pc; | ||
method.handled_exception_table[e].start_pc=start_pc; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
clang might complain here
/// which contains a table of the exceptions the method throws. | ||
void java_bytecode_parsert::rexceptions_attribute(methodt &method, const u4 &attribute_length) | ||
{ | ||
std::string name = method.name.c_str(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Unused variable
{ | ||
u2 exception_index_table=read_u2(); | ||
pool_entryt pool_entry_temp=pool_entry_lambda(exception_index_table); | ||
const irep_idt temp = constant(exception_index_table).type().get(ID_C_base_name); |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
src/util/std_types.h
Outdated
@@ -767,6 +767,8 @@ class code_typet:public typet | |||
class parametert; | |||
typedef std::vector<parametert> parameterst; | |||
|
|||
typedef std::vector<irept> exceptionst; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Shouldn't that be in java_method_typet
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is. It's just done in a later commit. If you view all of the files changed, there are no changes to std_types in this PR.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not a fan of typedefs like this one. It's not much shorter than a fully qualified vector and it gives you less information when it's explicitly specified,
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Then these changes should be squashed. Adding code and fixing it up within the same PR is rather confusing.
@@ -1049,7 +1049,7 @@ codet java_bytecode_convert_methodt::convert_instructions( | |||
i_it->statement=="monitorexit"))) | |||
{ | |||
const std::vector<unsigned int> handler = | |||
try_catch_handler(i_it->address, method.exception_table); | |||
try_catch_handler(i_it->address, method.handled_exception_table); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure about this one. How many exception tables are there?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There are two. There this one which deals with exceptions that can be caught. And the one that I am parsing in this PR which are exceptions that a method throws. Strictly speaking, in the bytecode, this is called exception_table and mine is also called exception_table. I thought this just made it a bit clearer what is what.
src/util/std_types.h
Outdated
@@ -767,6 +767,8 @@ class code_typet:public typet | |||
class parametert; | |||
typedef std::vector<parametert> parameterst; | |||
|
|||
typedef std::vector<irept> exceptionst; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not a fan of typedefs like this one. It's not much shorter than a fully qualified vector and it gives you less information when it's explicitly specified,
new_symbol_table.lookup_ref("java::ChildClass"); | ||
const java_class_typet java_class1 = | ||
to_java_class_type(class_symbol1.type); | ||
REQUIRE(java_class1.get_super_class() == "ParentClass"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
FYI: You can have multiple THEN
and WHEN
sections. That way you'll end up with more smaller tests. The benefit (apart from better variable names and shorter test body) is if one of the asserts below fails, all others will still be checked independently.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR failed Diffblue compatibility checks (cbmc commit: 6dde5dc).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/79889334
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
return pool_entry(index); | ||
}; | ||
|
||
if (number_of_exceptions == 0) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this necessary? Surely, if the number of exceptions is 0, then the loop below will loop 0 times and the control flow will leave this function anyway.
return; | ||
for(size_t i = 0; i < number_of_exceptions; i++) | ||
{ | ||
u2 exception_index_table=read_u2(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hint: Needs clang formatting, due to the lack of spaces around the =
.
{ | ||
u2 exception_index_table=read_u2(); | ||
pool_entryt pool_entry_temp=pool_entry_lambda(exception_index_table); | ||
const irep_idt temp = constant(exception_index_table).type().get(ID_C_base_name); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
temp
isn't a fantastic variable name. I guess this should be something like exception_name
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
oversight.
@@ -587,6 +587,13 @@ void java_bytecode_convert_methodt::convert( | |||
method_symbol.location=m.source_location; | |||
method_symbol.location.set_function(method_identifier); | |||
|
|||
code_typet::exceptionst &exceptions_list = code_type.throws_exceptions(); | |||
for(const auto &p : m.throws_exception_table) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I dislike using just p
a variable name. Having the type (if it is short) can also be handy. Maybe const irep_idt &exception_name
here would be good?
const code_typet method = to_code_type(method_symbol.type); | ||
const std::vector<irept> exceptions = method.throws_exceptions(); | ||
REQUIRE(id2string(exceptions.at(0).id()) == "CustomException"); | ||
REQUIRE(id2string(exceptions.at(1).id()) == "java.io.IOException"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we actually rely on the ordering here and is the ordering actually important? Maybe checking if exceptions
contains the exception which we are checking for, would be more robust.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This resize
bit is dubious. I'd like to see tests regrouped to allow more specific failures.
jbmc/src/java_bytecode/java_types.h
Outdated
|
||
inline java_method_typet &to_java_method_type(typet &type) | ||
{ | ||
assert(type.id()==ID_code); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should java_method_typet have its own ID_
tag?
Use invariants/precondition over asserts. Asserts are usually disabled in release builds.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not sure. It's not required here. ID_code is what is intended.
method.throws_exception_table.push_back(temp); | ||
} | ||
} | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There are so many unused variables, the body of this function could be rewritten as:
const u2 number_of_exceptions = read_u2();
for(size_t i = 0; i < number_of_exceptions; i++)
method.throws_exception_table.push_back(
constant(read_u2()).type().get(ID_C_base_name));
I'm not sure about .resize()
- do you want to shrink the vector, fill it with empty elements or .reserve()
elements to make push_back more efficient (in which case it's not worth it here I think)?
Rather than passing the method as an argument, you could return a vetor of constants. Right now it's not clear whether you're appending exceptions to an existing vector or creating new one from scratch. This forces the reader to look elsewhere whether this vector contains anything or not.
Also, this function doesn't seem to modify the state, so could be marked as const
, but for that you'd have to mark read_u2
and read_bytes
as const (I tried that, and it compiles).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I forgot to delete the pool entry when I used constant, so this is resolved.
I've taken your advice of returning a vector. Everything else is a void method, so it ruins the beauty of the declarations.
ALL the things are const.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually, not everything is const. There were some methods further down the chain that were required to be const and couldn't be.
for(const auto &p : m.throws_exception_table) | ||
{ | ||
if(!p.empty()) | ||
exceptions_list.push_back(irept(p)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The disadvantage of typedef
comes into play here. If they weren't used, it would've never occurred to you to convert irept
to irept
.
This function could be rewritten as std::copy_if
.
{ | ||
std::string name = method.name.c_str(); | ||
u2 number_of_exceptions = read_u2(); | ||
method.throws_exception_table.resize(number_of_exceptions); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this is actually introducing problems which you have to deal with later.
If my understanding of how this rexceptions_attribute
function is working is correct, then it is creating number_of_exceptions
empty entries in the throws_exception_table
and then adding the actual exceptions after this. Resulting in a vector which is twice as long as you expect, which contains junk empty items.
If you delete this line, then there will be no empty exceptions in the vector and you won't need to check for empty names when you get them out later.
u2 number_of_exceptions = read_u2(); | ||
method.throws_exception_table.resize(number_of_exceptions); | ||
|
||
const auto pool_entry_lambda = [this](u2 index) -> pool_entryt & { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this pool_entry_lambda
is making the code harder to read. Why not use pool_entry(exception_index_table)
inline, instead of pool_entry_lambda(exception_index_table)
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've done this another way, so this is no longer required.
00c5189
to
07b5faa
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR failed Diffblue compatibility checks (cbmc commit: 00c5189).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80118123
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
07b5faa
to
7cf4d1e
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR failed Diffblue compatibility checks (cbmc commit: 07b5faa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80122234
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: 7cf4d1e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80126073
7cf4d1e
to
b4e3609
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: b4e3609).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80199423
b4e3609
to
93f9708
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: 93f9708).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80285131
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd really like to see the interface of java_method_typet
changed before this gets merged if it isn't too hard.
@@ -151,7 +152,7 @@ class java_bytecode_parsert:public parsert | |||
} | |||
} | |||
|
|||
u8 read_bytes(size_t bytes) | |||
u8 read_bytes(size_t bytes) const |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not entirely sure about adding const
here (is it in right commit? This class is responsible for reading a file, read_bytes advances the "head" of where we're reading from. Don't understand why in->get()
is const
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah I see this was under the advice of @LAJW - feel free to disregard my comment, me and Lukasz can discuss and reach a conclusion.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've removed them for now because the function that I was trying to make const
could not be const
anyway. This was a byproduct of that and I left it in because it seemed sensible, but I don't want to muddy it up if there is uncertainty. It's not required for my PR.
new_symbol_table.lookup_ref("java::ThrowsExceptions.test:()V"); | ||
const code_typet method = to_code_type(method_symbol.type); | ||
const std::vector<irept> exceptions = method.throws_exceptions(); | ||
REQUIRE(exceptions.size() == 2); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: you can use Catch:Matchers::Vector
to do this in a nicer way - when I have an IDE I can show you a snippet, else you can search the code base for use cases. Not blocking but makes unit test and errors from it nicer to read.
irept("java.io.IOException")) != exceptions.end()); | ||
} | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please add a test for empty exception list
jbmc/src/java_bytecode/java_types.h
Outdated
class java_method_typet : public code_typet | ||
{ | ||
public: | ||
const std::vector<irept> &throws_exceptions() const |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I strongly dislike returning vector<irept>
as caller knows literaly nothing about what those irept
s might be, could be symbol_typet
as in bases()
on a class, or just strings as they actually are. To hide the implementation detail, I suggest changing to:
const std::vector<irep_idt> &throws_exceptions() const
{
std:vector<irep_idt>exceptions;
std::transform(
find(ID_exceptions_thrown_list).get_sub().being(),
find(ID_exceptions_thrown_list).get_sub().end(),
irept::idt);
return exceptions;
}
There may (must??) be a nicer way of doing this without the copy, but to me even this is preferable to an interface that returns essentially a typeless array.
I'd also try and get rid of the setter, and instead take a std::vector<irep_idt>
in the constructor so it is always in a valid state.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OK I see the constructor part is not possible without some restructuring. Instead I suggest a add_throws_exception
method that adds to the sub, since that is the only way anyone should be modifying it. (by giving the whole sub tree away, any caller could inadvertently remove all the exceptions).
|
||
inline const java_method_typet &to_java_method_type(const typet &type) | ||
{ | ||
PRECONDITION(type.id() == ID_code); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To add a bit more type safety, you might want to add a ID_C_java_method_type
so a caller can be sure that it really is a java_method_typet
not a code_typet
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why would this be a comment with C_
in the name instead of ID_java_method_type
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Consistency with other types, which isn't a great reason. I think you're probably right in fact, if I have a C style function pointer that probably shouldn't be treated equivalently to a static java function that doesn't throw any exceptions.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This has been added in #2661
jbmc/src/java_bytecode/java_types.h
Outdated
return exceptions; | ||
} | ||
|
||
void add_throws_exceptions(irept exception) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Make this an irep_idt
to completely hide the irept
from the public interface.
08ea814
to
93cfe02
Compare
This better reflects the bytecode.
4.7.5. The Exceptions Attribute
This is so that we do not need to have java-specific fields and related methods, like those relating to throws exceptions, in std_types
93cfe02
to
66ba3db
Compare
66ba3db
to
655248a
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR failed Diffblue compatibility checks (cbmc commit: 66ba3db).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80483614
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A thing to bear in mind in future, every symbol has two names, (e.g. java.io.Exception
vs. java::java.io.Exception
)
When you return an irep_idt
it isn't obvious which one you're getting back. I think leave for now, but it might be better to return symbol_typet
which implies you can look it up in the symbol table (and therefore definitely the java::java.io.Exception
. We've not been consistent about this in the past, but I think we should try to be in future.
std::find( | ||
exceptions.begin(), | ||
exceptions.end(), | ||
irept("CustomException").id()) != exceptions.end()); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No need to construct an irept and then get the id()
CI failure looked like a glitch so restarted. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: 655248a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80493176
6a10f1a Merge pull request diffblue#2462 from tautschnig/vs-goto-inline 96fc7b1 Merge pull request diffblue#2654 from peterschrammel/update-jml8 1847066 Update jbmc/lib/java-models-library to java-models-library#8 (remove sun.* imports) c157ba7 Revert "CMake version.cpp: switch back to add_custom_target" 7a009d6 Merge pull request diffblue#2650 from diffblue/aws-codebuild-clcache 63652fc add clcache to Windows build 6f72b3b Merge pull request diffblue#2657 from smowton/smowton/fix/cmake-version-cpp 35d09d5 CMake version.cpp: switch back to add_custom_target 80331d8 Merge pull request diffblue#2638 from diffblue/CBMC_VERSION_string 7c066f9 Merge pull request diffblue#2618 from owen-jones-diffblue/doc/move-irep-docs-from-util-to-irep ad5c375 use a string instead of macro for version number b6258db Merge pull request diffblue#2509 from danpoe/feature/sharing-map-stats eb71a01 Merge pull request diffblue#2639 from thk123/array-element-type c5519ec Merge pull request diffblue#2640 from allredj/support-for-load-containing-class-only 0855872 Address review comments diffblue#2 eaa7664 Wrap lines properly e682eb9 Add \ref in lots of places 3023cca Address review comments 758f069 Move dstringt documentation to above dstringt a54c82d Move documentation of irept to be above irept b827ea4 Use type equality check in unit tests 77185fd Merge pull request diffblue#2607 from jeannielynnmoulton/jeannie/ParseThrownExceptions2 1f4ef40 Add class loader debug output 4ae8eb6 Move sharing map friends declarations to unit tests 186897c Sharing stats for the sharing map 4438b43 Fix sharing map internal assertion 332febe Remove wrong sharing map internal assertions be7e140 Activate internal checks for the sharing map unit tests 713d3fe Merge pull request diffblue#2636 from polgreen/fix_function_map 87f90ee Add replace_all string utility ea2d393 Make test work on windows 4fa9943 Make array element type be not a comment 655248a Add unit test for when there are no exceptions. a6e7c4b Refactors interface for exceptions to not use irepts. 1134bba Creates java_method_typet which extends code_typet aa83622 Unit tests method get_super_class 565c999 Unit tests throws exceptions parsing. eb88509 Use parsed information for thrown exceptions. 5c7dcac Parses the exception attribute 7fcc42d Adds const to get/set_outer_class 5994dd8 Add method to get super class from java class type. fbad2d9 Rename variable extends to super_class 6d0776f if function is not in the function map, treat as if it has no body da86bdb Merge pull request diffblue#2602 from diffblue/__CPROVER_r/w_ok 0202f34 refactor pointer_validity_check using address_check 4a24ad4 use __CPROVER_r/w_ok in string.c library 732ce2a expand __CPROVER_r/w_ok in goto_check acfea65 __CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end 0618f7d Merge pull request diffblue#2628 from diffblue/clang-extensions 5e43131 Merge pull request diffblue#2608 from diffblue/ms_cl_int64 7c56091 Merge pull request diffblue#2634 from qaphla/local_bitvector_analysis_regression 44ef8d5 Merge pull request diffblue#2630 from diffblue/invalid-pointer-flattening f74c161 test for __float80 and __float128 8288a72 __float80 is a typedef, not a keyword 5495625 FreeBSD: default flavor is now CLANG e63402e added _Null_unspecified clang extension 16a49a7 bugfix: __float128 3849bb0 rename APPLE flavor to CLANG 060b59c separate pointer check for integer addresses 9b5847e fix flattening of ID_invalid_pointer 432dcf1 Added a regression test checking that --pointer-check does not generate excess checks if local_bitvector_analysis can gather information on the pointer being checked. cbfcc5c added support for _int64 keyword 0148347 Avoid signed/unsigned casts and conversion in goto_inline git-subtree-dir: cbmc git-subtree-split: 6a10f1a
get_super_class()
from a java class type. The bytecode was already parsed for this, but never sensibly stored as far as I could tell.throws
inmethodName() throws Exception1, Exception2
java_method_typet
which extendscode_typet
so that the methods involving exceptions which are java specific do not pollutecode_typet
(and the way we use it,java_method_typet
is semantically more correct). I would appreciate suggestions for what else could be moved into this, but will address those in another PR.This information will be used in test-gen to print the exceptions a test method throws more precisely, i.e., instead of
throws Throwable
it will bethrows SpecificException, AnotherException
, but this is a work in progress yet....
test-gen bump: https://github.com/diffblue/test-gen/pull/2094