Loading...

Searching...

No Matches

report_traces.cpp File Reference

#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:

Functions

std::optional< exprt > address_to_lvalue (exprt src)

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.

std::optional< exprt > address_to_lvalue ( exprt src )

Definition at line 20 of file report_traces.cpp.

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.

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.

static exprt use_address_of ( exprt src )

static

Definition at line 63 of file report_traces.cpp.