cprover
Loading...
Searching...
No Matches
counterexample_found.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Counterexample Found
4
5Author: 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
19std::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
26class bv_pointers_widet;
27
28void 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:91
show_assignment
void show_assignment(const bv_pointers_widet &)
Definition counterexample_found.cpp:24
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
solver_types.h
Solver.