Skip to content

Fix segmentation fault when failing to lookup parameter names [depends-on: #4434] #4390

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

Fix segmentation fault when failing to lookup parameter names [depends-on: #4434] #4390

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions jbmc/regression/jbmc/nondet_propagation1/lazy-loading-bug.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
8 changes: 4 additions & 4 deletions jbmc/src/java_bytecode/java_entry_point.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down