cprover
goto_verifier.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Verifier Interface
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
13 #define CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
14 
15 #include <util/optional.h>
16 #include <util/options.h>
17 #include <util/ui_message.h>
18 
19 #include "properties.h"
20 
26 {
27 public:
28  goto_verifiert() = delete;
29  goto_verifiert(const goto_verifiert &) = delete;
30  virtual ~goto_verifiert() = default;
31 
38  virtual resultt operator()() = 0;
39 
41  virtual void report() = 0;
42 
45  {
46  return properties;
47  }
48 
49 protected:
51 
52  const optionst &options;
56 };
57 
58 #endif // CPROVER_GOTO_CHECKER_GOTO_VERIFIER_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
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
goto_verifiert
An implementation of goto_verifiert checks all properties in a goto model.
Definition: goto_verifier.h:26
optionst
Definition: options.h:23
optional.h
goto_verifiert::operator()
virtual resultt operator()()=0
Check whether all properties hold.
options.h
Options.
goto_verifiert::~goto_verifiert
virtual ~goto_verifiert()=default
goto_verifiert::goto_verifiert
goto_verifiert()=delete
goto_verifiert::options
const optionst & options
Definition: goto_verifier.h:52
goto_verifiert::report
virtual void report()=0
Report results.
goto_verifiert::goto_verifiert
goto_verifiert(const goto_verifiert &)=delete
goto_verifiert::get_properties
const propertiest & get_properties()
Returns the properties.
Definition: goto_verifier.h:44
properties.h
Properties.
goto_verifiert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: goto_verifier.h:53
goto_verifiert::properties
propertiest properties
Definition: goto_verifier.h:55
goto_verifiert::log
messaget log
Definition: goto_verifier.h:54
ui_message.h