CBMC
report_traces.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Report Traces
4 
5 Author: 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 
17 void 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
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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.