Skip to content

Commit 6d63e16

Browse files
committed
Fix segmentation fault when failing to lookup parameter names
Users should not be able to trigger segmentation faults.
1 parent 42a2c73 commit 6d63e16

File tree

2 files changed

+16
-4
lines changed

2 files changed

+16
-4
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
andNot_Bug.class
3+
--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
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
--
8+
--
9+
This somewhat bogus test (both andNot_Pass.class and andNot_Bug.class are
10+
specified on the command line) resulted in a segmentation fault when used with
11+
symex-driven-lazy-loading. Even though that's a bogus command line, user input
12+
should never trigger a segmentation fault.

jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -488,16 +488,16 @@ static code_blockt record_pointer_parameters(
488488
for(std::size_t param_number = 0; param_number < parameters.size();
489489
param_number++)
490490
{
491-
const symbolt &p_symbol =
492-
*symbol_table.lookup(parameters[param_number].get_identifier());
491+
const symbolt *p_symbol =
492+
symbol_table.lookup(parameters[param_number].get_identifier());
493493

494-
if(!can_cast_type<pointer_typet>(p_symbol.type))
494+
if(!p_symbol || !can_cast_type<pointer_typet>(p_symbol->type))
495495
continue;
496496

497497
codet output(ID_output);
498498
output.operands().resize(2);
499499
output.op0() = address_of_exprt(index_exprt(
500-
string_constantt(p_symbol.base_name), from_integer(0, index_type())));
500+
string_constantt(p_symbol->base_name), from_integer(0, index_type())));
501501
output.op1() = arguments[param_number];
502502
output.add_source_location() = function.location;
503503

0 commit comments

Comments
 (0)