cprover
|
#include <counterexample_beautification.h>
Public Member Functions | |
virtual | ~counterexample_beautificationt () |
void | operator() (bv_cbmct &bv_cbmc, const symex_target_equationt &equation, const namespacet &ns) |
Protected Member Functions | |
void | get_minimization_list (prop_convt &prop_conv, const symex_target_equationt &equation, minimization_listt &minimization_list) |
void | minimize (const exprt &expr, class prop_minimizet &prop_minimize) |
symex_target_equationt::SSA_stepst::const_iterator | get_failed_property (const prop_convt &prop_conv, const symex_target_equationt &equation) |
Protected Attributes | |
symex_target_equationt::SSA_stepst::const_iterator | failed |
Definition at line 23 of file counterexample_beautification.h.
|
inlinevirtual |
Definition at line 26 of file counterexample_beautification.h.
References get_failed_property(), get_minimization_list(), minimize(), and operator()().
|
protected |
Definition at line 63 of file counterexample_beautification.cpp.
References tvt::is_false(), tvt::is_true(), prop_convt::l_get(), and symex_target_equationt::SSA_steps.
Referenced by operator()(), and ~counterexample_beautificationt().
|
protected |
Definition at line 22 of file counterexample_beautification.cpp.
References failed, irept::id(), tvt::is_false(), prop_convt::l_get(), symex_target_equationt::SSA_steps, and symex_targett::STATE.
Referenced by operator()(), and ~counterexample_beautificationt().
|
protected |
Referenced by ~counterexample_beautificationt().
void counterexample_beautificationt::operator() | ( | bv_cbmct & | bv_cbmc, |
const symex_target_equationt & | equation, | ||
const namespacet & | ns | ||
) |
Definition at line 81 of file counterexample_beautification.cpp.
References messaget::eom(), failed, get_failed_property(), messaget::get_message_handler(), get_minimization_list(), symex_targett::HIDDEN, prop_minimizet::objective(), messaget::set_message_handler(), boolbvt::set_to(), symex_target_equationt::SSA_steps, and messaget::status().
Referenced by ~counterexample_beautificationt().
|
protected |
Definition at line 50 of file counterexample_beautification.h.
Referenced by get_minimization_list(), and operator()().