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>
56 case ERROR:
return "ERROR";
78 std::vector<exprt> tmp;
98 #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 &)
This class represents an instruction in the GOTO intermediate representation.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::string status_string() const
enum bmc_all_propertiest::goalt::statust status
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
goalt(const goto_programt::instructiont &instruction)
std::map< irep_idt, goalt > goal_mapt
Bounded Model Checking for ANSI-C + HDL.
source_locationt source_location
The location of the instruction in the source file.
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)
#define UNREACHABLE
This should be used to mark dead code.
Cover a set of goals incrementally.
Bounded model checking or path exploration for goto-programs.
Try to cover some given set of goals incrementally.
const irep_idt & get_comment() const
source_locationt source_location
std::vector< symex_target_equationt::SSA_stepst::iterator > instancest