Invalid Java byte-code errors not handled

[NathanJPhillips]

There are many instances where invalid java byte-code input is not handled. Either it triggers a failed assertion in CBMC (leading to an abort or undefined behaviour if NDEBUG is set - see #182) or else wrong information is silently returned.
An example can be seen at https://github.com/diffblue/cbmc/blob/master/src/java_bytecode/java_types.cpp#L349

[tautschnig]

Fix it?

[NathanJPhillips]

@jgwilson42: @tautschnig suggests we fix all these errors. Once I've finished my current tasks can we organise it so that I can come off security for a week or so to go through and do this?

[tautschnig]

I obviously don't have any management insight, but the comments in both #182 and in here rather read like complaints than action plans. Complaints should be left to users, developers will hopefully produce patches -- do-ocracy.

[NathanJPhillips]

That's useful to hear. Hopefully we'll find a route through those who do have management responsibility to get to the point where I can get some time allocated to do some do-ing on these! Some of those people, like you I'm sure, are quite sympathetic to these needs.

[jgwilson42]

Thanks for the comments, I will look at how we can prioritise your time @NathanJPhillips.