CBMC
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< exprtaddress_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.