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
25
class
goto_verifiert
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
44
const
propertiest
&
get_properties
()
45
{
46
return
properties
;
47
}
48
49
protected
:
50
goto_verifiert
(
const
optionst
&,
ui_message_handlert
&);
51
52
const
optionst
&
options
;
53
ui_message_handlert
&
ui_message_handler
;
54
messaget
log
;
55
propertiest
properties
;
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
goto-checker
goto_verifier.h
Generated by
1.8.20