We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 85405bb commit 6473900Copy full SHA for 6473900
jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -1241,7 +1241,16 @@ static void notify_static_method_calls(
1241
const symbol_exprt *fn_sym =
1242
expr_try_dynamic_cast<symbol_exprt>(call_expr.function());
1243
if(fn_sym)
1244
- needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
+ {
1245
+ INVARIANT(
1246
+ false,
1247
+ "Java synthetic methods are not "
1248
+ "expected to produce side_effect_expr_function_callt. If "
1249
+ "that has changed, remove this invariant. Also note that "
1250
+ "as of the time of writing remove_virtual_functions did "
1251
+ "not support this form of function call.");
1252
+ // needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
1253
+ }
1254
}
1255
1256
0 commit comments