Skip to content

Commit

Permalink
pretty-print expression instructions
Browse files Browse the repository at this point in the history
This adds pretty-printing for goto-program expression instructions.
  • Loading branch information
kroening committed Jul 5, 2022
1 parent c00319e commit 09e1041
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 2 deletions.
4 changes: 2 additions & 2 deletions regression/goto-instrument/remove-calls-no-body2/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ main.c
^VERIFICATION SUCCESSFUL$
func3\(\)
func4\(\)
567\)
285\)
567$
285$
ret1 :=.*nondet.*
--
func1\(.*\)
Expand Down
5 changes: 5 additions & 0 deletions src/goto-programs/goto_program.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,11 @@ std::ostream &goto_programt::instructiont::output(std::ostream &out) const
<< '\n';
break;
}
else if(code.get_statement() == ID_expression)
{
out << "EXPRESSION " << format(code.op0()) << '\n';
break;
}
else if(code.get_statement() == ID_havoc_object)
{
out << "HAVOC_OBJECT " << format(code.op0()) << '\n';
Expand Down

0 comments on commit 09e1041

Please sign in to comment.