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

This graph shows which files directly or indirectly include this file:

Functions
void	show_program (const namespacet &ns, const symex_target_equationt &equation)
	Print the steps of `equation` on the standard output. More...

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.h.

Function Documentation

◆ 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_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.

Functions

Detailed Description

Function Documentation

◆ show_byte_ops()

◆ show_program()