File tree 2 files changed +21
-0
lines changed
regression/jbmc/context-include-exclude 2 files changed +21
-0
lines changed Original file line number Diff line number Diff line change
1
+ CORE
2
+ Main.class
3
+ --context-exclude 'org.cprover.MyClass$Inner.' --function 'org.cprover.MyClass$Inner.doIt:(I)I'
4
+ ^EXIT=6$
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.
Original file line number Diff line number Diff line change @@ -899,6 +899,16 @@ bool java_bytecode_languaget::generate_support_functions(
899
899
// parameter names
900
900
convert_lazy_method (res.main_function .name , symbol_table_builder);
901
901
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
+
902
912
// generate the test harness in __CPROVER__start and a call the entry point
903
913
return java_entry_point (
904
914
symbol_table_builder,
You can’t perform that action at this time.
0 commit comments