12 #ifndef CPROVER_CBMC_ALL_PROPERTIES_CLASS_H 13 #define CPROVER_CBMC_ALL_PROPERTIES_CLASS_H 39 typedef std::vector<symex_target_equationt::SSA_stepst::iterator>
55 case ERROR:
return "ERROR";
64 const goto_programt::instructiont &instruction):
67 description=
id2string(instruction.source_location.get_comment());
76 std::vector<exprt> tmp;
77 tmp.reserve(instances.size());
78 for(
const auto &inst : instances)
96 #endif // CPROVER_CBMC_ALL_PROPERTIES_CLASS_H
const goto_functionst & goto_functions
const std::string & id2string(const irep_idt &d)
safety_checkert::resultt operator()()
virtual void do_before_solving()
virtual void goal_covered(const cover_goalst::goalt &)
exprt conjunction(const exprt::operandst &op)
std::string status_string() const
enum bmc_all_propertiest::goalt::statust status
goalt(const goto_programt::instructiont &instruction)
std::map< irep_idt, goalt > goal_mapt
Bounded Model Checking for ANSI-C + HDL.
Base class for all expressions.
virtual void report(const cover_goalst &cover_goals)
bmc_all_propertiest(const goto_functionst &_goto_functions, prop_convt &_solver, bmct &_bmc)
Cover a set of goals incrementally.
Try to cover some given set of goals incrementally.
std::vector< symex_target_equationt::SSA_stepst::iterator > instancest