cprover
|
#include <graphml_witness.h>
Public Member Functions | |
graphml_witnesst (const namespacet &_ns) | |
void | operator() (const goto_tracet &goto_trace) |
counterexample witness More... | |
void | operator() (const symex_target_equationt &equation) |
proof witness More... | |
const graphmlt & | graph () |
Protected Member Functions | |
void | remove_l0_l1 (exprt &expr) |
std::string | convert_assign_rec (const irep_idt &identifier, const code_assignt &assign) |
Protected Attributes | |
const namespacet & | ns |
graphmlt | graphml |
Definition at line 21 of file graphml_witness.h.
|
inlineexplicit |
Definition at line 24 of file graphml_witness.h.
|
protected |
Definition at line 47 of file graphml_witness.cpp.
References base_type_eq(), struct_union_typet::components(), namespace_baset::follow(), forall_operands, from_expr(), from_integer(), has_prefix(), irept::id(), id2string(), index_type(), code_assignt::lhs(), ns, exprt::operands(), remove_l0_l1(), code_assignt::rhs(), typet::subtype(), to_array_type(), to_byte_extract_expr(), to_member_expr(), to_struct_union_type(), and exprt::type().
Referenced by operator()().
|
inline |
Definition at line 32 of file graphml_witness.h.
References graphml.
Referenced by bmct::output_graphml().
void graphml_witnesst::operator() | ( | const goto_tracet & | goto_trace | ) |
counterexample witness
Definition at line 174 of file graphml_witness.cpp.
References grapht< N >::add_node(), goto_trace_stept::ASSERT, goto_trace_stept::ASSIGNMENT, goto_trace_stept::ASSUME, goto_trace_stept::ATOMIC_BEGIN, goto_trace_stept::ATOMIC_END, goto_trace_stept::CONSTRAINT, convert_assign_rec(), xmlt::data, goto_trace_stept::DEAD, goto_trace_stept::DECL, filter_out(), from_expr(), goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, source_locationt::get_file(), source_locationt::get_line(), goto_trace_stept::GOTO, graphml, has_prefix(), id2string(), grapht< N >::in(), goto_trace_stept::INPUT, graphmlt::key_values, goto_trace_stept::LOCATION, goto_trace_stept::MEMORY_BARRIER, xmlt::new_element(), goto_trace_stept::NONE, ns, grapht< N >::out(), goto_trace_stept::OUTPUT, xmlt::set_attribute(), goto_trace_stept::SHARED_READ, goto_trace_stept::SHARED_WRITE, goto_trace_stept::SPAWN, and goto_tracet::steps.
void graphml_witnesst::operator() | ( | const symex_target_equationt & | equation | ) |
proof witness
Definition at line 358 of file graphml_witness.cpp.
References grapht< N >::add_node(), goto_trace_stept::ASSERT, goto_trace_stept::ASSIGNMENT, goto_trace_stept::ASSUME, goto_trace_stept::ATOMIC_BEGIN, goto_trace_stept::ATOMIC_END, goto_trace_stept::CONSTRAINT, convert_assign_rec(), xmlt::data, goto_trace_stept::DEAD, goto_trace_stept::DECL, dstringt::empty(), from_expr(), goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, source_locationt::get_file(), source_locationt::get_line(), goto_trace_stept::GOTO, graphml, id2string(), grapht< N >::in(), goto_trace_stept::INPUT, source_locationt::is_built_in(), irept::is_nil(), graphmlt::key_values, goto_trace_stept::LOCATION, goto_trace_stept::MEMORY_BARRIER, xmlt::new_element(), goto_trace_stept::NONE, ns, grapht< N >::out(), goto_trace_stept::OUTPUT, xmlt::set_attribute(), goto_trace_stept::SHARED_READ, goto_trace_stept::SHARED_WRITE, goto_trace_stept::SPAWN, and symex_target_equationt::SSA_steps.
|
protected |
Definition at line 21 of file graphml_witness.cpp.
References Forall_operands, ssa_exprt::get_original_expr(), irept::id(), id2string(), is_ssa_expr(), symbol_exprt::set_identifier(), size_type(), to_ssa_expr(), and to_symbol_expr().
Referenced by convert_assign_rec().
|
protected |
Definition at line 39 of file graphml_witness.h.
Referenced by graph(), and operator()().
|
protected |
Definition at line 38 of file graphml_witness.h.
Referenced by convert_assign_rec(), and operator()().