ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
goto_trace.cpp File Reference
#include <cassert>
#include <cstring>
#include <goto-symex/trace/goto_trace.h>
#include <goto-symex/trace/printf_formatter.h>
#include <goto-symex/witness/witnesses.h>
#include <regex>
#include <langapi/language_util.h>
#include <langapi/languages.h>
#include <util/arith/arith_tools.h>
#include <util/base/cwe_mapping.h>
#include <util/irep/std_types.h>
#include <optional>
#include <ostream>
Include dependency graph for goto_trace.cpp:

Functions

void counterexample_value (std::ostream &out, const namespacet &ns, const expr2tc &lhs, const expr2tc &value)
void show_goto_trace_gui (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
bool input_file_check (const locationt &l)
static std::string witness_origin_file (const locationt &loc, const std::string &verified_file)
static BigInt witness_start_line (const locationt &loc, const std::string &verified_file, optionst &options)
static std::string witness_waypoint_file (const locationt &loc, const std::string &verified_file)
static waypoint witness_waypoint (const locationt &loc, const std::string &verified_file, optionst &options)
static const locationt * witness_input_location (const goto_trace_stept &step)
static waypoint witness_target_waypoint (const goto_trace_stept &step, const std::string &verified_file, optionst &options)
void show_state_header (std::ostream &out, const goto_trace_stept &state, const locationt &location, unsigned step_nr, const bool simplify_trace)
static std::string format_nondet_reads (const namespacet &ns, const goto_trace_stept &step)
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.
static std::optional< waypoint > witness_nondet_waypoint (const namespacet &ns, const goto_trace_stept &step, const std::string &verified_file, optionst &options)
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 appendInfo (std::string &dest, const std::string &label, const std::string &value)
void show_simplified_location (std::ostream &out, const locationt &location)
static const irep_idt & frame_function_name (const namespacet &ns, const irep_idt &id)
void show_goto_trace (std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, bool reachability_trace)

Function Documentation

◆ appendInfo()

void appendInfo ( std::string & dest,
const std::string & label,
const std::string & value )

◆ 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 & lhs,
const expr2tc & value )

◆ format_nondet_reads()

std::string format_nondet_reads ( const namespacet & ns,
const goto_trace_stept & step )
static

◆ frame_function_name()

const irep_idt & frame_function_name ( const namespacet & ns,
const irep_idt & id )
static

◆ 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_tracewhen 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 )

◆ show_state_header()

void show_state_header ( std::ostream & out,
const goto_trace_stept & state,
const locationt & location,
unsigned step_nr,
const bool simplify_trace )

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

◆ witness_input_location()

const locationt * witness_input_location ( const goto_trace_stept & step)
static

◆ witness_nondet_waypoint()

std::optional< waypoint > witness_nondet_waypoint ( const namespacet & ns,
const goto_trace_stept & step,
const std::string & verified_file,
optionst & options )
static

◆ witness_origin_file()

std::string witness_origin_file ( const locationt & loc,
const std::string & verified_file )
static

◆ witness_start_line()

BigInt witness_start_line ( const locationt & loc,
const std::string & verified_file,
optionst & options )
static

◆ witness_target_waypoint()

waypoint witness_target_waypoint ( const goto_trace_stept & step,
const std::string & verified_file,
optionst & options )
static

◆ witness_waypoint()

waypoint witness_waypoint ( const locationt & loc,
const std::string & verified_file,
optionst & options )
static

◆ witness_waypoint_file()

std::string witness_waypoint_file ( const locationt & loc,
const std::string & verified_file )
static