Skip to content

Commit 6bb3b0c

Browse files
Document show_program.h
No functional change.
1 parent e3f7deb commit 6bb3b0c

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

src/goto-symex/show_program.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,14 @@ Author: Daniel Kroening, [email protected]
1515
class namespacet;
1616
class symex_target_equationt;
1717

18+
/// Print the steps of \p equation on the standard output.
19+
///
20+
/// For each step, prints the location, then if the step is an assignment,
21+
/// assertion, assume, constraint, shared read or shared write:
22+
/// prints an instruction counter, followed by the instruction type, and the
23+
/// current guard if it is not equal to true.
24+
/// \param ns: namespace
25+
/// \param equation: SSA form of the program
1826
void show_program(const namespacet &ns, const symex_target_equationt &equation);
1927

2028
#endif // CPROVER_GOTO_SYMEX_SHOW_PROGRAM_H

0 commit comments

Comments
 (0)