show_program.cpp File Reference

#include "show_program.h"
#include <fstream>
#include <iostream>
#include <goto-symex/symex_target_equation.h>
#include <langapi/language_util.h>
#include <util/byte_operators.h>
#include <util/json_irep.h>
#include <util/ui_message.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...
template<typename expr_typet >
std::size_t	count_expr_typed (const exprt &expr)
bool	duplicated_previous_step (const SSA_stept &ssa_step)
void	show_ssa_step_plain (messaget::mstreamt &out, const namespacet &ns, const SSA_stept &ssa_step, const exprt &ssa_expr)
json_objectt	get_ssa_step_json (const namespacet &ns, const SSA_stept &ssa_step, const exprt &ssa_expr)
template<typename expr_typet >
void	show_byte_op_plain (messaget::mstreamt &out, const namespacet &ns, const symex_target_equationt &equation)
template<typename expr_typet >
std::string	json_get_key_byte_op_list ()
template<typename expr_typet >
std::string	json_get_key_byte_op_num ()
template<typename expr_typet >
json_objectt	get_byte_op_json (const namespacet &ns, const symex_target_equationt &equation)
template<typename expr_typet >
std::string	json_get_key_byte_op_stats ()
bool	is_outfile_specified (const optionst &options)
void	show_byte_ops_plain (ui_message_handlert &ui_message_handler, std::ostream &out, bool outfile_given, const namespacet &ns, const symex_target_equationt &equation)
void	show_byte_ops_json (std::ostream &out, const namespacet &ns, const symex_target_equationt &equation)
void	show_byte_ops_xml (ui_message_handlert &ui_message_handler)
void	show_byte_ops (const optionst &options, ui_message_handlert &ui_message_handler, const namespacet &ns, const symex_target_equationt &equation)
	Count and display all byte extract and byte update operations from equation on standard output or file. More...

Detailed Description

Output of the program (SSA) constraints

Definition in file show_program.cpp.

Function Documentation

count_expr_typed()

template<typename expr_typet >

std::size_t count_expr_typed

(

const exprt &

expr

)

Definition at line 91 of file show_program.cpp.

duplicated_previous_step()

bool duplicated_previous_step

(

const SSA_stept &

ssa_step

)

Definition at line 106 of file show_program.cpp.

get_byte_op_json()

template<typename expr_typet >

json_objectt get_byte_op_json	(	const namespacet &	ns,
		const symex_target_equationt &	equation
	)

Definition at line 207 of file show_program.cpp.

get_ssa_step_json()

json_objectt get_ssa_step_json	(	const namespacet &	ns,
		const SSA_stept &	ssa_step,
		const exprt &	ssa_expr
	)

Definition at line 129 of file show_program.cpp.

is_outfile_specified()

bool is_outfile_specified

(

const optionst &

options

)

Definition at line 261 of file show_program.cpp.

json_get_key_byte_op_list()

template<typename expr_typet >

std::string json_get_key_byte_op_list

(

)

Definition at line 184 of file show_program.cpp.

json_get_key_byte_op_num()

template<typename expr_typet >

std::string json_get_key_byte_op_num

(

)

Definition at line 195 of file show_program.cpp.

json_get_key_byte_op_stats()

template<typename expr_typet >

std::string json_get_key_byte_op_stats

(

)

Definition at line 251 of file show_program.cpp.

show_byte_op_plain()

template<typename expr_typet >

void show_byte_op_plain	(	messaget::mstreamt &	out,
		const namespacet &	ns,
		const symex_target_equationt &	equation
	)

Definition at line 150 of file show_program.cpp.

show_byte_ops()

void show_byte_ops	(	const optionst &	options,
		ui_message_handlert &	ui_message_handler,
		const namespacet &	ns,
		const symex_target_equationt &	equation
	)

Count and display all byte extract and byte update operations from equation on standard output or file.

The name of the output file is given by the outfile option from options, the standard output is used if it is not provided. The format is either JSON or plain text depending on ui_message_handler; XML is not supported. For each step, if it's a byte extract or update, print location, ssa expression and compute number of extracts/updates in total in the equation.

Parameters

options	parsed options
ui_message_handler	ui message handler
ns	namespace
equation	SSA form of the program

Definition at line 323 of file show_program.cpp.

show_byte_ops_json()

void show_byte_ops_json	(	std::ostream &	out,
		const namespacet &	ns,
		const symex_target_equationt &	equation
	)

Definition at line 296 of file show_program.cpp.

show_byte_ops_plain()

void show_byte_ops_plain	(	ui_message_handlert &	ui_message_handler,
		std::ostream &	out,
		bool	outfile_given,
		const namespacet &	ns,
		const symex_target_equationt &	equation
	)

Definition at line 267 of file show_program.cpp.

show_byte_ops_xml()

void show_byte_ops_xml

(

ui_message_handlert &

ui_message_handler

)

Definition at line 313 of file show_program.cpp.

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

ns	namespace
equation	SSA form of the program

Definition at line 61 of file show_program.cpp.

show_ssa_step_plain()

void show_ssa_step_plain	(	messaget::mstreamt &	out,
		const namespacet &	ns,
		const SSA_stept &	ssa_step,
		const exprt &	ssa_expr
	)

Definition at line 114 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

ns	Namespace
step	SSA step
annotation	Additonal information to include in step output
count	Step number, incremented after output

Definition at line 30 of file show_program.cpp.