CBMC
counterexample_found.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Counterexample Found
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPROVER_COUNTEREXAMPLE_FOUND_H
13 #define CPROVER_CPROVER_COUNTEREXAMPLE_FOUND_H
14 
15 #include "solver_types.h"
16 
17 #include <unordered_set>
18 
19 std::optional<propertyt::tracet> counterexample_found(
20  const std::vector<framet> &,
21  const workt &,
22  const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
23  bool verbose,
24  const namespacet &);
25 
26 class bv_pointers_widet;
27 
28 void show_assignment(const bv_pointers_widet &);
29 
30 #endif // CPROVER_CPROVER_COUNTEREXAMPLE_FOUND_H
address_taken
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Definition: address_taken.cpp:51
bv_pointers_widet
Definition: bv_pointers_wide.h:20
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
counterexample_found
std::optional< propertyt::tracet > counterexample_found(const std::vector< framet > &, const workt &, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &)
Definition: counterexample_found.cpp:173
show_assignment
void show_assignment(const bv_pointers_widet &)
Definition: counterexample_found.cpp:24
solver_types.h
Solver.