From f123ae9e94aa3f5542c7872de63c2cb931c066e2 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 7 Feb 2018 11:37:11 +0000 Subject: [PATCH] Adding comment referencing where the invariant comes from --- src/java_bytecode/java_bytecode_parser.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 0db26a5ec06..93dba637f5a 100644 --- 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 "