Skip to content

Commit 7663540

Browse files
committed
as_string() on instructions now takes function identifier
1 parent f527eaa commit 7663540

File tree

3 files changed

+6
-4
lines changed

3 files changed

+6
-4
lines changed

src/goto-programs/goto_program.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -399,6 +399,7 @@ std::list<exprt> objects_written(
399399

400400
std::string as_string(
401401
const class namespacet &ns,
402+
const irep_idt &function,
402403
const goto_programt::instructiont &i)
403404
{
404405
std::string result;
@@ -412,7 +413,7 @@ std::string as_string(
412413
if(!i.guard.is_true())
413414
{
414415
result+="IF "
415-
+from_expr(ns, i.function, i.guard)
416+
+from_expr(ns, function, i.guard)
416417
+" THEN ";
417418
}
418419

@@ -435,7 +436,7 @@ std::string as_string(
435436
case DEAD:
436437
case FUNCTION_CALL:
437438
case ASSIGN:
438-
return from_expr(ns, i.function, i.code);
439+
return from_expr(ns, function, i.code);
439440

440441
case ASSUME:
441442
case ASSERT:
@@ -444,7 +445,7 @@ std::string as_string(
444445
else
445446
result+="ASSERT ";
446447

447-
result+=from_expr(ns, i.function, i.guard);
448+
result+=from_expr(ns, function, i.guard);
448449

449450
{
450451
const irep_idt &comment=i.source_location.get_comment();

src/goto-programs/goto_program.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -813,6 +813,7 @@ std::list<exprt> expressions_written(const goto_programt::instructiont &);
813813

814814
std::string as_string(
815815
const namespacet &ns,
816+
const irep_idt &function,
816817
const goto_programt::instructiont &);
817818

818819
#endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H

src/goto-programs/goto_trace.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -284,7 +284,7 @@ void show_state_header(
284284

285285
if(options.show_code)
286286
{
287-
out << as_string(ns, *state.pc)
287+
out << as_string(ns, state.function, *state.pc)
288288
<< "\n";
289289
out << "----------------------------------------------------"
290290
<< "\n";

0 commit comments

Comments
 (0)