Fix segmentation fault when failing to lookup parameter names

Users should not be able to trigger segmentation faults.

Author: tautschnig

jbmc/regression/jbmc/nondet_propagation1/lazy-loading-bug.desc

@@ -0,0 +1,13 @@
+CORE
+andNot_Bug.class
+--depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --max-nondet-string-length 100 andNot_Pass.class --function andNot_Pass.main
+^\*\* 1 of \d+ failed
+VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This somewhat bogus test (both andNot_Pass.class and andNot_Bug.class are
+specified on the command line) resulted in a segmentation fault when used with
+symex-driven-lazy-loading. Even though that's a bogus command line, user input
+should never trigger a segmentation fault.

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -492,16 +492,16 @@ static code_blockt record_pointer_parameters(
   for(std::size_t param_number = 0; param_number < parameters.size();
       param_number++)
   {
-    const symbolt &p_symbol =
-      *symbol_table.lookup(parameters[param_number].get_identifier());
+    const symbolt *p_symbol =
+      symbol_table.lookup(parameters[param_number].get_identifier());
 
-    if(!can_cast_type<pointer_typet>(p_symbol.type))
+    if(!p_symbol || !can_cast_type<pointer_typet>(p_symbol->type))
       continue;
 
     codet output(ID_output);
     output.operands().resize(2);
     output.op0() = address_of_exprt(index_exprt(
-      string_constantt(p_symbol.base_name), from_integer(0, index_type())));
+      string_constantt(p_symbol->base_name), from_integer(0, index_type())));
     output.op1() = arguments[param_number];
     output.add_source_location() = function.location;