Skip to content

Commit e36d7d8

Browse files
Check if object is nil before writing trace
We were accessing fields of the expression without first checking that it is not nil which could lead to invalid memory access
1 parent 6b519ad commit e36d7d8

File tree

1 file changed

+1
-7
lines changed

1 file changed

+1
-7
lines changed

src/goto-programs/goto_trace.cpp

+1-7
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ void goto_trace_stept::output(
9191

9292
out << "\n";
9393

94-
if(pc->is_other() || pc->is_assign())
94+
if((pc->is_other() && lhs_object.is_not_nil()) || pc->is_assign())
9595
{
9696
irep_idt identifier=lhs_object.get_object_name();
9797
out << " " << from_expr(ns, identifier, lhs_object.get_original_expr())
@@ -386,14 +386,8 @@ void show_goto_trace(
386386
break;
387387

388388
case goto_trace_stept::typet::CONSTRAINT:
389-
UNREACHABLE;
390-
break;
391-
392389
case goto_trace_stept::typet::SHARED_READ:
393390
case goto_trace_stept::typet::SHARED_WRITE:
394-
UNREACHABLE;
395-
break;
396-
397391
default:
398392
UNREACHABLE;
399393
}

0 commit comments

Comments
 (0)