CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
goto_verifier.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Verifier Interface
4
5Author: 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 "properties.h"
16
17#include <util/message.h>
18
19class optionst;
21
27{
28public:
29 goto_verifiert() = delete;
30 goto_verifiert(const goto_verifiert &) = delete;
31 virtual ~goto_verifiert() = default;
32
39 virtual resultt operator()() = 0;
40
42 virtual void report() = 0;
43
46 {
47 return properties;
48 }
49
50protected:
52
57};
58
59#endif // CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
An implementation of goto_verifiert checks all properties in a goto model.
virtual resultt operator()()=0
Check whether all properties hold.
virtual void report()=0
Report results.
goto_verifiert(const goto_verifiert &)=delete
propertiest properties
const propertiest & get_properties()
Returns the properties.
goto_verifiert()=delete
const optionst & options
virtual ~goto_verifiert()=default
ui_message_handlert & ui_message_handler
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
Properties.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76
resultt
The result of goto verifying.
Definition properties.h:45