Skip to content

Commit 8dd731b

Browse files
committed
Use regex to test nondet method name
1 parent 96060b1 commit 8dd731b

File tree

1 file changed

+11
-5
lines changed

1 file changed

+11
-5
lines changed

src/java_bytecode/java_bytecode_convert_method.cpp

+11-5
Original file line numberDiff line numberDiff line change
@@ -483,6 +483,10 @@ void java_bytecode_convert_methodt::convert(
483483
if((!m.is_abstract) && (!m.is_native))
484484
method_symbol.value=convert_instructions(m, code_type);
485485

486+
#ifdef DEBUG
487+
std::cerr << method_symbol.value.pretty() << '\n';
488+
#endif
489+
486490
remove_assert_after_generic_nondet(method_symbol.value);
487491

488492
// Replace the existing stub symbol with the real deal:
@@ -1300,12 +1304,14 @@ codet java_bytecode_convert_methodt::convert_instructions(
13001304
results[0].add_source_location()=i_it->source_location;
13011305
}
13021306

1303-
else if(statement=="invokestatic" &&
1304-
has_prefix(id2string(arg0.get(ID_identifier)),
1305-
"java::org.cprover.CProver.nondetWith") &&
1306-
!working_set.empty())
1307+
else if(
1308+
statement=="invokestatic" &&
1309+
std::regex_match(
1310+
id2string(arg0.get(ID_identifier)),
1311+
std::regex(
1312+
".*org.cprover.CProver.(nondetWithNull|nondetWithoutNull).*")) &&
1313+
!working_set.empty())
13071314
{
1308-
// Currently unused.
13091315
const auto working_set_begin=working_set.begin();
13101316
const auto next_address=address_map.find(*working_set_begin);
13111317
assert(next_address!=address_map.end());

0 commit comments

Comments
 (0)