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;
44 
45  // if failed, we compute a goto_trace for the first failing instance
48 
49  std::string status_string() const
50  {
51  switch(status)
52  {
53  case UNKNOWN: return "UNKNOWN";
54  case FAILURE: return "FAILURE";
55  case SUCCESS: return "SUCCESS";
56  case ERROR: return "ERROR";
57  }
58 
59  // make some poor compilers happy
61  return "";
62  }
63 
64  explicit goalt(
65  const goto_programt::instructiont &instruction):
67  {
68  source_location = instruction.source_location;
70  }
71 
73  {
74  }
75 
76  exprt as_expr() const
77  {
78  std::vector<exprt> tmp;
79  tmp.reserve(instances.size());
80  for(const auto &inst : instances)
81  tmp.push_back(literal_exprt(inst->cond_literal));
82  return conjunction(tmp);
83  }
84  };
85 
86  typedef std::map<irep_idt, goalt> goal_mapt;
88 
89 protected:
93 
94  virtual void report(const cover_goalst &cover_goals);
95  virtual void do_before_solving() {}
96 };
97 
98 #endif // CPROVER_CBMC_ALL_PROPERTIES_CLASS_H
const goto_functionst & goto_functions
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:178
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:50
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 &#39;level&#39;.
Definition: message.h:144
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:187
Base class for all expressions.
Definition: expr.h:54
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.
Definition: invariant.h:478
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:150
const irep_idt & get_comment() const
std::vector< symex_target_equationt::SSA_stepst::iterator > instancest