12 #ifndef CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H 13 #define CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H 47 #endif // CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H Generate Equation using Symbolic Execution.
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
void remove_l0_l1(exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
graphml_witnesst(const namespacet &_ns)
Base class for all expressions.
Read/write graphs as GraphML.
void operator()(const goto_tracet &goto_trace)
counterexample witness
A codet representing an assignment in the program.