cprover
all_properties_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_ALL_PROPERTIES_CLASS_H
13 #define CPROVER_CBMC_ALL_PROPERTIES_CLASS_H
14 
16 
17 #include "bmc.h"
18 
21  public messaget
22 {
23 public:
25  const goto_functionst &_goto_functions,
26  prop_convt &_solver,
27  bmct &_bmc):
28  goto_functions(_goto_functions), solver(_solver), bmc(_bmc)
29  {
30  }
31 
33 
34  virtual void goal_covered(const cover_goalst::goalt &);
35 
36  struct goalt
37  {
38  // a property holds if all instances of it are true
39  typedef std::vector<symex_target_equationt::SSA_stepst::iterator>
42  std::string description;
43 
44  // if failed, we compute a goto_trace for the first failing instance
47 
48  std::string status_string() const
49  {
50  switch(status)
51  {
52  case UNKNOWN: return "UNKNOWN";
53  case FAILURE: return "FAILURE";
54  case SUCCESS: return "SUCCESS";
55  case ERROR: return "ERROR";
56  }
57 
58  // make some poor compilers happy
60  return "";
61  }
62 
63  explicit goalt(
64  const goto_programt::instructiont &instruction):
66  {
68  }
69 
71  {
72  }
73 
74  exprt as_expr() const
75  {
76  std::vector<exprt> tmp;
77  tmp.reserve(instances.size());
78  for(const auto &inst : instances)
79  tmp.push_back(literal_exprt(inst->cond_literal));
80  return conjunction(tmp);
81  }
82  };
83 
84  typedef std::map<irep_idt, goalt> goal_mapt;
86 
87 protected:
91 
92  virtual void report(const cover_goalst &cover_goals);
93  virtual void do_before_solving() {}
94 };
95 
96 #endif // CPROVER_CBMC_ALL_PROPERTIES_CLASS_H
const goto_functionst & goto_functions
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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.
Definition: goto_program.h:173
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
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.
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
Base class for all expressions.
Definition: expr.h:42
virtual void report(const cover_goalst &cover_goals)
bmc_all_propertiest(const goto_functionst &_goto_functions, prop_convt &_solver, bmct &_bmc)
#define UNREACHABLE
Definition: invariant.h:250
Cover a set of goals incrementally.
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
const irep_idt & get_comment() const
std::vector< symex_target_equationt::SSA_stepst::iterator > instancest