Skip to content

Commit 47fe36f

Browse files
Changed main_function_resultt to use an enum instead of a collection of bools
Fix comment
1 parent a084a6a commit 47fe36f

File tree

4 files changed

+16
-23
lines changed

4 files changed

+16
-23
lines changed

src/java_bytecode/ci_lazy_methods.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -60,9 +60,9 @@ bool ci_lazy_methodst::operator()(
6060
std::vector<irep_idt> method_worklist1;
6161
std::vector<irep_idt> method_worklist2;
6262

63-
auto main_function=
63+
main_function_resultt main_function=
6464
get_main_symbol(symbol_table, main_class, get_message_handler(), true);
65-
if(main_function.stop_convert)
65+
if(main_function.status!=main_function_resultt::Success)
6666
{
6767
// Failed, mark all functions in the given main class(es)
6868
// reachable.

src/java_bytecode/java_bytecode_language.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -248,8 +248,8 @@ bool java_bytecode_languaget::generate_support_functions(
248248
{
249249
main_function_resultt res=
250250
get_main_symbol(symbol_table, main_class, get_message_handler());
251-
if(res.stop_convert)
252-
return res.error_found;
251+
if(res.status!=main_function_resultt::Success)
252+
return res.status==main_function_resultt::Error;
253253

254254
// generate the test harness in __CPROVER__start and a call the entry point
255255
return

src/java_bytecode/java_entry_point.cpp

+11-17
Original file line numberDiff line numberDiff line change
@@ -345,8 +345,7 @@ main_function_resultt get_main_symbol(
345345
message.error() << "main symbol resolution failed: "
346346
<< error_message << messaget::eom;
347347
res.main_function=symbol;
348-
res.error_found=true;
349-
res.stop_convert=true;
348+
res.status=main_function_resultt::Error;
350349
return res;
351350
}
352351

@@ -364,8 +363,7 @@ main_function_resultt get_main_symbol(
364363
message.error() << "main method `" << main_class
365364
<< "' has no body" << messaget::eom;
366365
res.main_function=symbol;
367-
res.error_found=true;
368-
res.stop_convert=true;
366+
res.status=main_function_resultt::Error;
369367
return res;
370368
}
371369
}
@@ -378,8 +376,7 @@ main_function_resultt get_main_symbol(
378376
if(main_class.empty())
379377
{
380378
res.main_function=symbol;
381-
res.error_found=false;
382-
res.stop_convert=true;
379+
res.status=main_function_resultt::NotFound;
383380
return res; // silently ignore
384381
}
385382

@@ -405,8 +402,7 @@ main_function_resultt get_main_symbol(
405402
{
406403
// Not found, silently ignore
407404
res.main_function=symbol;
408-
res.error_found=false;
409-
res.stop_convert=true;
405+
res.status=main_function_resultt::NotFound;
410406
return res;
411407
}
412408

@@ -415,8 +411,7 @@ main_function_resultt get_main_symbol(
415411
message.error() << "main method in `" << main_class
416412
<< "' is ambiguous" << messaget::eom;
417413
res.main_function=symbolt();
418-
res.error_found=true;
419-
res.stop_convert=true;
414+
res.status=main_function_resultt::Error;
420415
return res; // give up with error, no main
421416
}
422417

@@ -429,16 +424,15 @@ main_function_resultt get_main_symbol(
429424
message.error() << "main method `" << main_class
430425
<< "' has no body" << messaget::eom;
431426
res.main_function=symbol;
432-
res.error_found=true;
433-
res.stop_convert=true;
427+
res.status=main_function_resultt::Error;
434428
return res; // give up with error
435429
}
436430
}
437431

432+
// Return found function
438433
res.main_function=symbol;
439-
res.error_found=false;
440-
res.stop_convert=false;
441-
return res; // give up with error
434+
res.status=main_function_resultt::Success;
435+
return res;
442436
}
443437

444438
/// Given the \p symbol_table and the \p main_class to test, this function
@@ -491,8 +485,8 @@ bool java_entry_point(
491485
messaget message(message_handler);
492486
main_function_resultt res=
493487
get_main_symbol(symbol_table, main_class, message_handler);
494-
if(res.stop_convert)
495-
return res.stop_convert;
488+
if(res.status!=main_function_resultt::Success)
489+
return true;
496490
symbolt symbol=res.main_function;
497491

498492
assert(!symbol.value.is_nil());

src/java_bytecode/java_entry_point.h

+1-2
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,8 @@ bool java_entry_point(
2828

2929
typedef struct
3030
{
31+
enum { Success, Error, NotFound } status;
3132
symbolt main_function;
32-
bool error_found;
33-
bool stop_convert;
3433
} main_function_resultt;
3534

3635
/// Figures out the entry point of the code to verify

0 commit comments

Comments
 (0)