cprover
incremental_goto_checker.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Incremental Goto Checker Interface
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H
13 #define CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H
14 
15 #include <util/ui_message.h>
16 
17 #include "properties.h"
18 
19 class goto_tracet;
20 class optionst;
21 
34 {
35 public:
38  virtual ~incremental_goto_checkert() = default;
39 
40  struct resultt
41  {
42  enum class progresst
43  {
46  FOUND_FAIL,
49  DONE
50  };
51 
53 
54  resultt() = delete;
55  explicit resultt(progresst);
56 
59  std::unordered_set<irep_idt> updated_properties;
60  };
61 
78  virtual resultt operator()(propertiest &properties) = 0;
79 
82  virtual void report()
83  {
84  }
85 
86 protected:
88 
89  const optionst &options;
92 };
93 
94 #endif // CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
ui_message_handlert
Definition: ui_message.h:20
incremental_goto_checkert::resultt
Definition: incremental_goto_checker.h:41
optionst
Definition: options.h:23
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:89
incremental_goto_checkert::resultt::progresst
progresst
Definition: incremental_goto_checker.h:43
incremental_goto_checkert::log
messaget log
Definition: incremental_goto_checker.h:91
incremental_goto_checkert::resultt::resultt
resultt()=delete
incremental_goto_checkert::resultt::progresst::FOUND_FAIL
@ FOUND_FAIL
The goto checker may be able to find another FAILed property if operator() is called again.
incremental_goto_checkert::incremental_goto_checkert
incremental_goto_checkert(const incremental_goto_checkert &)=delete
incremental_goto_checkert::operator()
virtual resultt operator()(propertiest &properties)=0
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
incremental_goto_checkert::resultt::progresst::DONE
@ DONE
The goto checker has returned all results for the given set of properties.
incremental_goto_checkert
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
Definition: incremental_goto_checker.h:34
incremental_goto_checkert::incremental_goto_checkert
incremental_goto_checkert()=delete
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
incremental_goto_checkert::resultt::progress
progresst progress
Definition: incremental_goto_checker.h:52
incremental_goto_checkert::resultt::updated_properties
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
Definition: incremental_goto_checker.h:59
properties.h
Properties.
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:90
incremental_goto_checkert::~incremental_goto_checkert
virtual ~incremental_goto_checkert()=default
incremental_goto_checkert::report
virtual void report()
Additional reporting that may result from the underlying solver, no-op by default.
Definition: incremental_goto_checker.h:82
ui_message.h