cprover
goto-symex/module.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \defgroup module_goto-symex Symbolic Execution & Counterexample Production
3 
4 \author Kareem Khazem
5 
6 **Key classes:**
7 * goto_symex_statet
8 * goto_symext
9 
10 \dot
11 digraph G {
12  node [shape=box];
13  rankdir="LR";
14  1 [shape=none, label=""];
15  2 [label="goto conversion"];
16  3 [shape=none, label=""];
17  1 -> 2 [label="goto-programs, goto-functions, symbol table"];
18  2 -> 3 [label="equations"];
19 }
20 \enddot
21 
22 ---
23 \section counter-example-production Counter Example Production
24 
25 In the \ref goto-symex directory.
26 
27 **Key classes:**
28 * symex_target_equationt
29 * prop_convt
30 * \ref bmct
31 * fault_localizationt
32 * counterexample_beautificationt
33 
34 \dot
35 digraph G {
36  node [shape=box];
37  rankdir="LR";
38  1 [shape=none, label=""];
39  2 [label="goto conversion"];
40  3 [shape=none, label=""];
41  1 -> 2 [label="solutions"];
42  2 -> 3 [label="counter-examples"];
43 }
44 \enddot