CBMC
Loading...
Searching...
No Matches
graphml_witness.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Witnesses for Traces and Proofs
4
5Author: Daniel Kroening
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
13#define CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
14
15#include <xmllang/graphml.h>
16
17class code_assignt;
18class exprt;
19class goto_tracet;
20class namespacet;
22
24{
25public:
27 : ns(_ns)
28 {
29 }
30
32 void operator()(const symex_target_equationt &equation);
33
34 const graphmlt &graph()
35 {
36 return graphml;
37 }
38
39protected:
40 const namespacet &ns;
42
43 void remove_l0_l1(exprt &expr);
44 std::string convert_assign_rec(
45 const irep_idt &identifier,
46 const code_assignt &assign);
47
48 template <typename T>
49 static void hash_combine(std::size_t &seed, const T &v)
50 {
51 std::hash<T> hasher;
52 seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
53 }
54
55 template <typename S, typename T>
56 struct pair_hash // NOLINT(readability/identifiers)
57 {
58 std::size_t operator()(const std::pair<S, T> &v) const
59 {
60 std::size_t seed = 0;
61 hash_combine(seed, v.first);
62 hash_combine(seed, v.second);
63 return seed;
64 }
65 };
66 std::unordered_map<
67 std::pair<unsigned int, const irept::dt *>,
68 std::string,
71};
72
73#endif // CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A goto_instruction_codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
Trace of a GOTO program.
Definition goto_trace.h:177
const namespacet & ns
static void hash_combine(std::size_t &seed, const T &v)
void operator()(const goto_tracet &goto_trace)
counterexample witness
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
const graphmlt & graph()
graphml_witnesst(const namespacet &_ns)
void remove_l0_l1(exprt &expr)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Read/write graphs as GraphML.
#define hash_combine(h1, h2)
Definition irep_hash.h:121
std::size_t operator()(const std::pair< S, T > &v) const