Merge pull request #1796 from thk123/refactor/bytecode-parsing-tidy

Java Bytecode parsing tidy

Author: kroening

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -45,6 +45,9 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_set>
 #include <regex>
 
+/// Given a string of the format '?blah?', will return true when compared
+/// against a string that matches appart from any characters that are '?'
+/// in the original string. Equivalent to doing a regex match on '.blah.'
 class patternt
 {
 public:

src/java_bytecode/java_bytecode_parser.cpp

@@ -79,6 +79,7 @@ class java_bytecode_parsert:public parsert
     if(index==0 || index>=constant_pool.size())
     {
       error() << "invalid constant pool index (" << index << ")" << eom;
+      error() << "constant pool size: " << constant_pool.size() << eom;
       throw 0;
     }
 
@@ -946,6 +947,12 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
     {
       u2 start_pc=read_u2();
       u2 end_pc=read_u2();
+
+      INVARIANT(
+        start_pc < end_pc,
+        "The start_pc must be less than the end_pc as this is the range the "
+        "exception is active");
+
       u2 handler_pc=read_u2();
       u2 catch_type=read_u2();
       method.exception_table[e].start_pc=start_pc;