show_vcc.cpp File Reference

Output of the verification conditions (VCCs) More...

#include "show_vcc.h"
#include <util/exception_utils.h>
#include <util/format_expr.h>
#include <util/json_irep.h>
#include <util/ui_message.h>
#include "symex_target_equation.h"
#include <fstream>
#include <iostream>

Include dependency graph for show_vcc.cpp:

Go to the source code of this file.

Functions
static void	show_vcc_plain (messaget::mstreamt &out, const symex_target_equationt &equation)
	Output equations from equation in plain text format to the given output stream out. More...
static void	show_vcc_json (std::ostream &out, const symex_target_equationt &equation)
	Output equations from equation in the JSON format to the given output stream out. More...
void	show_vcc (const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
	Output equations from equation to a file or to the standard output. More...

Detailed Description

Output of the verification conditions (VCCs)

Definition in file show_vcc.cpp.

Function Documentation

show_vcc()

void show_vcc	(	const optionst &	options,
		ui_message_handlert &	ui_message_handler,
		const symex_target_equationt &	equation
	)

Output equations from equation to a file or to the standard output.

The name of the output file is given by the outfile option from options, the standard input is used if it is not provided. The format is either JSON or plain text depending on ui_message_handler; XML is not supported. See show_vcc_json and show_vcc_plain

Definition at line 168 of file show_vcc.cpp.

show_vcc_json()

static void show_vcc_json ( std::ostream &  out, const symex_target_equationt &  equation  )

static

Output equations from equation in the JSON format to the given output stream out.

The format is an array vccs, containing fields:

• constraints, which is an array containing the constraints which apply to that equation
• expression, a string containing the formatted expression
• sourceLocation (optional), the corresponding location in the program
• comment (optional)

Definition at line 111 of file show_vcc.cpp.

show_vcc_plain()

static void show_vcc_plain ( messaget::mstreamt &  out, const symex_target_equationt &  equation  )

static

Output equations from equation in plain text format to the given output stream out.

Each equation is prefixed by a negative index, formatted {-N}

Definition at line 28 of file show_vcc.cpp.