CBMC
|
Solver. More...
#include "report_traces.h"
#include <util/console.h>
#include <util/format_expr.h>
#include <util/pointer_expr.h>
#include <iomanip>
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) |
Solver.
Definition in file report_traces.cpp.
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.
Definition at line 63 of file report_traces.cpp.