Skip to content

Commit c65874f

Browse files
committed
output "SET RETURN VALUE" when displaying goto programs
To avoid the impression that the 'set return value' instruction alters control flow, output "SET RETURN VALUE" instead of "RETURN" when displaying goto programs.
1 parent ce3fcaa commit c65874f

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/goto-programs/goto_program.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ std::ostream &goto_programt::output_instruction(
133133
break;
134134

135135
case SET_RETURN_VALUE:
136-
out << "RETURN " << format(instruction.return_value()) << '\n';
136+
out << "SET RETURN VALUE " << format(instruction.return_value()) << '\n';
137137
break;
138138

139139
case DECL:

0 commit comments

Comments
 (0)