B | |
| basicblocks_to_vertices [Llvmcfg] |
Get the vertices associated to some basicblocks.
|
| break_by_list [Llvmcfg] |
Similar to
Llvmcfg.break_graph, but allows the user to provide the list of node to be broken.
|
| break_graph [Llvmcfg] |
Break all the cycle in a graph, effectively returning a DAG.
|
E | |
| env [Llvm2smt.Init] |
Environment mapping llvm values (primed, or not) to smt values.
|
F | |
| fprint_graph [Smtgraph.Make.Dot] | |
| fprint_graph [Llvmcfg.Dot] | |
| from_llvm [Smtgraph.Make] | |
G | |
| get_block [Llvm2smt.Init] | |
| get_clauses [Smtgraph.Make] | |
| get_var [Llvm2smt.Init] | |
L | |
| llvm2smt [Llvm2smt.Init] |
Transform an Llvm graph into a formula graph, filling
env on the way.
|
O | |
| of_llfunction [Llvmcfg] |
Create the graph representing an llvm function.
|
| output_graph [Smtgraph.Make.Dot] | |
| output_graph [Llvmcfg.Dot] | |
S | |
| sprint_exn [Llvm2smt] | |
| sprint_exn_block [Llvm2smt] | |
| sprint_exn_var [Llvm2smt] | |
T | |
| to_smt [Smtgraph.Make] |
Gather all the formulas of the graph in one big smt formula.
|
V | |
| vertex [Llvmcfg] |