report_traces.cpp File Reference

Solver. More...

#include "report_traces.h"
#include <util/console.h>
#include <util/format_expr.h>
#include <util/pointer_expr.h>
#include <iomanip>

Include dependency graph for report_traces.cpp:

Go to the source code of this file.

Functions
std::optional< exprt >	address_to_lvalue (exprt src)
static exprt	use_address_of (exprt src)
void	show_trace (const std::vector< framet > &frames, const propertyt &property, bool verbose, const namespacet &ns)
void	report_traces (const std::vector< framet > &frames, const std::vector< propertyt > &properties, bool verbose, const namespacet &ns)

Detailed Description

Solver.

Definition in file report_traces.cpp.

Function Documentation

address_to_lvalue()

std::optional< exprt > address_to_lvalue

(

exprt

src

)

Definition at line 20 of file report_traces.cpp.

report_traces()

void report_traces	(	const std::vector< framet > &	frames,
		const std::vector< propertyt > &	properties,
		bool	verbose,
		const namespacet &	ns
	)

Definition at line 151 of file report_traces.cpp.

show_trace()

void show_trace	(	const std::vector< framet > &	frames,
		const propertyt &	property,
		bool	verbose,
		const namespacet &	ns
	)

Definition at line 72 of file report_traces.cpp.

use_address_of()

static exprt use_address_of ( exprt  src )

static

Definition at line 63 of file report_traces.cpp.