Skip to content

Commit bf9a8c2

Browse files
Load cproverNondetInitialize with lazy-methods
This allows cproverValidate to be loaded even when lazy methods is activated.
1 parent 54d943d commit bf9a8c2

File tree

1 file changed

+7
-1
lines changed

1 file changed

+7
-1
lines changed

src/java_bytecode/ci_lazy_methods_needed.cpp

+7-1
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,14 @@ bool ci_lazy_methods_neededt::add_needed_class(
3434
{
3535
if(!needed_classes.insert(class_symbol_name).second)
3636
return false;
37-
const irep_idt clinit_name(id2string(class_symbol_name)+".<clinit>:()V");
37+
const std::string &class_name_string = id2string(class_symbol_name);
38+
const irep_idt clinit_name(class_name_string + ".<clinit>:()V");
3839
if(symbol_table.symbols.count(clinit_name))
3940
add_needed_method(clinit_name);
41+
42+
const irep_idt cprover_validate(
43+
class_name_string + ".cproverNondetInitialize:()V");
44+
if(symbol_table.symbols.count(cprover_validate))
45+
add_needed_method(cprover_validate);
4046
return true;
4147
}

0 commit comments

Comments
 (0)