Merge pull request diffblue#1806 from thk123/refactor/address-review-…

…comments-from-1796 Adding comment referencing where the invariant comes from
smowton · Feb 16, 2018 · bb88574 · bb88574
2 parents db9c214 + f123ae9
commit bb88574
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp
@@ -948,6 +948,7 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
       u2 start_pc=read_u2();
       u2 end_pc=read_u2();
 
+      // from the class file format spec ("4.7.3. The Code Attribute" for Java8)
       INVARIANT(
         start_pc < end_pc,
         "The start_pc must be less than the end_pc as this is the range the "