#include <fstream>
#include <goto-programs/goto_program.h>
#include <goto-symex/equation/symex_target.h>
#include <map>
#include <irep2/irep2.h>
#include <util/irep/migrate.h>
#include <util/config/cmdline.h>
#include <vector>
#include <string_view>

Include dependency graph for goto_trace.h:

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

Classes
class	goto_trace_stept
class	goto_tracet

Functions
void	show_goto_trace_gui (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
void	show_goto_trace (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, bool reachability_trace=false)
bool	input_file_check (const locationt &l)
void	show_simplified_location (std::ostream &out, const locationt &location)
void	violation_graphml_goto_trace (optionst &options, const namespacet &ns, const goto_tracet &goto_trace, const std::string &output_path_override="")
	Emit a GraphML violation witness for `goto_trace`.
void	violation_yaml_goto_trace (optionst &options, const namespacet &ns, const goto_tracet &goto_trace, const std::string &output_path_override="")
	Emit a YAML violation witness for `goto_trace`; analogous to violation_graphml_goto_trace.
void	correctness_graphml_goto_trace (optionst &options, const namespacet &ns, const goto_tracet &goto_trace)
void	correctness_yaml_goto_trace (optionst &options, const namespacet &ns, const goto_tracet &goto_trace)
void	generate_goto_trace_in_correctness_graphml_format (std::string &witness_output, bool is_detailed_mode, int &specification, const namespacet &ns, const goto_tracet &goto_trace)
void	counterexample_value (std::ostream &out, const namespacet &ns, const expr2tc &identifier, const expr2tc &value)
void	generate_html_report (const std::string_view uuid, const namespacet &ns, const goto_tracet &goto_trace, const optionst &options)
void	generate_json_report (const std::string_view uuid, const namespacet &ns, const goto_tracet &goto_trace)

Function Documentation

◆ correctness_graphml_goto_trace()

void correctness_graphml_goto_trace	(	optionst &	options,
		const namespacet &	ns,
		const goto_tracet &	goto_trace )

◆ correctness_yaml_goto_trace()

void correctness_yaml_goto_trace	(	optionst &	options,
		const namespacet &	ns,
		const goto_tracet &	goto_trace )

◆ counterexample_value()

void counterexample_value	(	std::ostream &	out,
		const namespacet &	ns,
		const expr2tc &	identifier,
		const expr2tc &	value )

◆ generate_goto_trace_in_correctness_graphml_format()

void generate_goto_trace_in_correctness_graphml_format	(	std::string &	witness_output,
		bool	is_detailed_mode,
		int &	specification,
		const namespacet &	ns,
		const goto_tracet &	goto_trace )

◆ generate_html_report()

void generate_html_report	(	const std::string_view	uuid,
		const namespacet &	ns,
		const goto_tracet &	goto_trace,
		const optionst &	options )

◆ generate_json_report()

void generate_json_report	(	const std::string_view	uuid,
		const namespacet &	ns,
		const goto_tracet &	goto_trace )

◆ input_file_check()

bool input_file_check ( const locationt & l )

◆ show_goto_trace()

void show_goto_trace	(	std::ostream &	out,
		const namespacet &	ns,
		const goto_tracet &	goto_trace,
		bool	reachability_trace = false )

Parameters

reachability_trace when true the closing ASSERT step is rendered as a reached location rather than a violated property. Coverage runs use this: their assertions are probes whose falsifiability means "reachable", so labelling the trace a violation would be a false statement about the program (issue #6387).

◆ show_goto_trace_gui()

void show_goto_trace_gui	(	std::ostream &	out,
		const namespacet &	ns,
		const goto_tracet &	goto_trace )

◆ show_simplified_location()

void show_simplified_location	(	std::ostream &	out,
		const locationt &	location )

◆ violation_graphml_goto_trace()

void violation_graphml_goto_trace	(	optionst &	options,
		const namespacet &	ns,
		const goto_tracet &	goto_trace,
		const std::string &	output_path_override = "" )

Emit a GraphML violation witness for goto_trace.

When output_path_override is non-empty it overrides the path read from options["witness-output-graphml"]. Used by –all-witnesses to fan out per-witness filenames safely under –parallel-solving without mutating the shared options object.

◆ violation_yaml_goto_trace()

void violation_yaml_goto_trace	(	optionst &	options,
		const namespacet &	ns,
		const goto_tracet &	goto_trace,
		const std::string &	output_path_override = "" )

Emit a YAML violation witness for goto_trace; analogous to violation_graphml_goto_trace.

Classes

Functions