Skip to content

Commit 4bc0680

Browse files
committed
Add INVARIANT on declaring_class after method conversion
All symbols for methods should have a `declaring_class` after conversion. This commit adds INVARIANTs for this condition on returning from `java_bytecode_languaget::convert_single_method`, in order to demonstrate that this condition holds.
1 parent 23c30c1 commit 4bc0680

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1106,6 +1106,8 @@ bool java_bytecode_languaget::convert_single_method(
11061106
// function:
11071107
notify_static_method_calls(
11081108
to_code(writable_symbol.value), needed_lazy_methods);
1109+
INVARIANT(
1110+
declaring_class(writable_symbol), "Method must have a declaring class.");
11091111
return false;
11101112
}
11111113

@@ -1124,6 +1126,7 @@ bool java_bytecode_languaget::convert_single_method(
11241126
string_preprocess,
11251127
class_hierarchy,
11261128
threading_support);
1129+
INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
11271130
return false;
11281131
}
11291132

@@ -1147,6 +1150,7 @@ bool java_bytecode_languaget::convert_single_method(
11471150
needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
11481151
}
11491152

1153+
INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
11501154
return true;
11511155
}
11521156

0 commit comments

Comments
 (0)