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
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:72
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
conjunction
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
bmct
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
bmc_all_propertiest::goalt::source_location
source_locationt source_location
Definition: all_properties_class.h:43
prop_convt
Definition: prop_conv.h:27
bmc_all_propertiest::goal_map
goal_mapt goal_map
Definition: all_properties_class.h:87
bmc_all_propertiest::goalt::instancest
std::vector< symex_target_equationt::SSA_stepst::iterator > instancest
Definition: all_properties_class.h:40
bmc_all_propertiest::report
virtual void report(const cover_goalst &cover_goals)
Definition: all_properties.cpp:154
bmc_all_propertiest::goalt
Definition: all_properties_class.h:36
cover_goalst::observert
Definition: cover_goals.h:79
exprt
Base class for all expressions.
Definition: expr.h:54
bmc_all_propertiest::bmc_all_propertiest
bmc_all_propertiest(const goto_functionst &_goto_functions, prop_convt &_solver, bmct &_bmc)
Definition: all_properties_class.h:24
bmc_all_propertiest::do_before_solving
virtual void do_before_solving()
Definition: all_properties_class.h:95
bmc_all_propertiest::goalt::status
enum bmc_all_propertiest::goalt::statust status
cover_goalst
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
bmc_all_propertiest::goalt::goto_trace
goto_tracet goto_trace
Definition: all_properties_class.h:47
bmc_all_propertiest::goalt::SUCCESS
Definition: all_properties_class.h:46
bmc_all_propertiest::goal_mapt
std::map< irep_idt, goalt > goal_mapt
Definition: all_properties_class.h:86
bmc_all_propertiest::goalt::status_string
std::string status_string() const
Definition: all_properties_class.h:49
bmc_all_propertiest::goalt::UNKNOWN
Definition: all_properties_class.h:46
bmc_all_propertiest::goalt::FAILURE
Definition: all_properties_class.h:46
bmc_all_propertiest::operator()
safety_checkert::resultt operator()()
Definition: all_properties.cpp:50
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
literal_exprt
Definition: literal_expr.h:17
bmc_all_propertiest::goalt::ERROR
Definition: all_properties_class.h:46
bmc_all_propertiest::goalt::statust
statust
Definition: all_properties_class.h:46
bmc_all_propertiest::goalt::description
std::string description
Definition: all_properties_class.h:42
bmc.h
source_locationt
Definition: source_location.h:20
bmc_all_propertiest::goalt::goalt
goalt()
Definition: all_properties_class.h:72
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
safety_checkert::resultt
resultt
Definition: safety_checker.h:33
bmc_all_propertiest::solver
prop_convt & solver
Definition: all_properties_class.h:91
bmc_all_propertiest::goto_functions
const goto_functionst & goto_functions
Definition: all_properties_class.h:90
bmc_all_propertiest::goalt::goalt
goalt(const goto_programt::instructiont &instruction)
Definition: all_properties_class.h:64
goto_tracet
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
bmc_all_propertiest::goal_covered
virtual void goal_covered(const cover_goalst::goalt &)
Definition: all_properties.cpp:27
cover_goalst::goalt
Definition: cover_goals.h:38
bmc_all_propertiest
Definition: all_properties_class.h:19
cover_goals.h
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
bmc_all_propertiest::goalt::instances
instancest instances
Definition: all_properties_class.h:41
bmc_all_propertiest::goalt::as_expr
exprt as_expr() const
Definition: all_properties_class.h:76
bmc_all_propertiest::bmc
bmct & bmc
Definition: all_properties_class.h:92