Skip to content

Commit b590a06

Browse files
Error message when entry function body cannot be produced
This can happen when a body is not loaded. Previously crashed on a failed map.at
1 parent 69a9528 commit b590a06

File tree

2 files changed

+21
-0
lines changed

2 files changed

+21
-0
lines changed
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
Main.class
3+
--context-exclude 'org.cprover.MyClass$Inner.' --function 'org.cprover.MyClass$Inner.doIt:(I)I'
4+
^EXIT=1$
5+
^SIGNAL=0$
6+
the program has no entry point
7+
--
8+
_Map_base::at
9+
unordered_map::at: key not found
10+
--
11+
Tests that a proper error message is printed.

jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -899,6 +899,16 @@ bool java_bytecode_languaget::generate_support_functions(
899899
// parameter names
900900
convert_lazy_method(res.main_function.name, symbol_table_builder);
901901

902+
const symbolt &symbol =
903+
symbol_table_builder.lookup_ref(res.main_function.name);
904+
if(symbol.value.is_nil())
905+
{
906+
throw invalid_command_line_argument_exceptiont(
907+
"the program has no entry point",
908+
"function",
909+
"Specify an entry point that is in the analysis context");
910+
}
911+
902912
// generate the test harness in __CPROVER__start and a call the entry point
903913
return java_entry_point(
904914
symbol_table_builder,

0 commit comments

Comments
 (0)