cprover
show_program.cpp File Reference
#include "show_program.h"
#include <iostream>
#include <goto-symex/symex_target_equation.h>
#include <langapi/language_util.h>
+ Include dependency graph for show_program.cpp:

Go to the source code of this file.

Functions

static void show_step (const namespacet &ns, const SSA_stept &step, const std::string &annotation, std::size_t &count)
 Output a single SSA step. More...
 
void show_program (const namespacet &ns, const symex_target_equationt &equation)
 Print the steps of equation on the standard output. More...
 

Detailed Description

Output of the program (SSA) constraints

Definition in file show_program.cpp.

Function Documentation

◆ show_program()

void show_program ( const namespacet ns,
const symex_target_equationt equation 
)

Print the steps of equation on the standard output.

For each step, prints the location, then if the step is an assignment, assertion, assume, constraint, shared read or shared write: prints an instruction counter, followed by the instruction type, and the current guard if it is not equal to true.

Parameters
nsnamespace
equationSSA form of the program

Definition at line 53 of file show_program.cpp.

◆ show_step()

static void show_step ( const namespacet ns,
const SSA_stept step,
const std::string &  annotation,
std::size_t &  count 
)
static

Output a single SSA step.

Parameters
nsNamespace
stepSSA step
annotationAdditonal information to include in step output
countStep number, incremented after output

Definition at line 25 of file show_program.cpp.