CBMC
Loading...
Searching...
No Matches
report_traces.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Report Traces
4
5Author: Daniel Kroening <dkr@amazon.com>
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_CPROVER_REPORT_TRACES_H
13#define CPROVER_CPROVER_REPORT_TRACES_H
14
15#include "solver_types.h" // IWYU pragma: keep
16
17void report_traces(
18 const std::vector<framet> &frames,
19 const std::vector<propertyt> &properties,
20 bool verbose,
21 const namespacet &);
22
23#endif // CPROVER_CPROVER_REPORT_TRACES_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
report_traces
void report_traces(const std::vector< framet > &frames, const std::vector< propertyt > &properties, bool verbose, const namespacet &)
Definition report_traces.cpp:151
solver_types.h
Solver.