Output of the program (SSA) constraints. More...

#include "show_program.h"
#include <util/byte_operators.h>
#include <util/json_irep.h>
#include <util/ui_message.h>
#include <goto-symex/symex_target_equation.h>
#include <langapi/language_util.h>
#include <fstream>
#include <iostream>

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 90 of file show_program.cpp.

◆ duplicated_previous_step()

bool duplicated_previous_step ( const SSA_stept & ssa_step )

Definition at line 105 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 206 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 128 of file show_program.cpp.

◆ is_outfile_specified()

bool is_outfile_specified ( const optionst & options )

Definition at line 260 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 183 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 194 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 250 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 149 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 322 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 295 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 266 of file show_program.cpp.

◆ show_byte_ops_xml()

void show_byte_ops_xml ( ui_message_handlert & ui_message_handler )

Definition at line 312 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 60 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 113 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 29 of file show_program.cpp.

Functions

Detailed Description

Function Documentation

◆ count_expr_typed()

◆ duplicated_previous_step()

◆ get_byte_op_json()

◆ get_ssa_step_json()

◆ is_outfile_specified()

◆ json_get_key_byte_op_list()

◆ json_get_key_byte_op_num()

◆ json_get_key_byte_op_stats()

◆ show_byte_op_plain()

◆ show_byte_ops()

◆ show_byte_ops_json()

◆ show_byte_ops_plain()

◆ show_byte_ops_xml()

◆ show_program()

◆ show_ssa_step_plain()

◆ show_step()