Go to the documentation of this file.
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
Class that provides messages with a built-in verbosity 'level'.
const irep_idt & get_comment() const
source_locationt source_location
The location of the instruction in the source file.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Bounded model checking or path exploration for goto-programs.
source_locationt source_location
std::vector< symex_target_equationt::SSA_stepst::iterator > instancest
virtual void report(const cover_goalst &cover_goals)
Base class for all expressions.
bmc_all_propertiest(const goto_functionst &_goto_functions, prop_convt &_solver, bmct &_bmc)
virtual void do_before_solving()
Try to cover some given set of goals incrementally.
#define UNREACHABLE
This should be used to mark dead code.
std::map< irep_idt, goalt > goal_mapt
std::string status_string() const
safety_checkert::resultt operator()()
const std::string & id2string(const irep_idt &d)
A collection of goto functions.
const goto_functionst & goto_functions
goalt(const goto_programt::instructiont &instruction)
virtual void goal_covered(const cover_goalst::goalt &)
This class represents an instruction in the GOTO intermediate representation.
enum bmc_all_propertiest::goalt::statust status