cprover
property_checker.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Property Checker Interface
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
13
#define CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
14
15
// this is just an interface -- it won't actually do any checking!
16
17
#include <
util/message.h
>
18
19
#include "
goto_trace.h
"
20
#include "
goto_model.h
"
21
22
class
property_checkert
:
public
messaget
23
{
24
public
:
25
property_checkert
()
26
{
27
}
28
29
explicit
property_checkert
(
30
message_handlert
&_message_handler);
31
32
enum class
resultt
{
PASS
,
FAIL
,
ERROR
,
UNKNOWN
};
33
34
static
std::string
as_string
(
resultt
);
35
36
// Check whether all properties in goto_functions hold.
37
virtual
resultt
operator()
(
const
goto_modelt
&)=0;
38
39
struct
property_statust
40
{
41
// this is the counterexample
42
goto_tracet
error_trace
;
43
resultt
result
;
44
goto_programt::const_targett
location
;
45
};
46
47
// the irep_idt is the property id
48
typedef
std::map<irep_idt, property_statust>
property_mapt
;
49
property_mapt
property_map
;
50
51
protected
:
52
void
initialize_property_map
(
const
goto_functionst
&);
53
};
54
55
#endif // CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition:
message.h:144
property_checkert::property_map
property_mapt property_map
Definition:
property_checker.h:49
property_checkert::property_statust::location
goto_programt::const_targett location
Definition:
property_checker.h:44
goto_model.h
goto_modelt
Definition:
goto_model.h:24
property_checkert::operator()
virtual resultt operator()(const goto_modelt &)=0
goto_trace.h
property_checkert::initialize_property_map
void initialize_property_map(const goto_functionst &)
Definition:
property_checker.cpp:33
property_checkert::resultt::PASS
property_checkert
Definition:
property_checker.h:22
message_handlert
Definition:
message.h:24
property_checkert::property_mapt
std::map< irep_idt, property_statust > property_mapt
Definition:
property_checker.h:48
property_checkert::property_checkert
property_checkert()
Definition:
property_checker.h:25
property_checkert::resultt::FAIL
property_checkert::property_statust::result
resultt result
Definition:
property_checker.h:43
property_checkert::property_statust
Definition:
property_checker.h:39
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:22
property_checkert::resultt::ERROR
property_checkert::resultt::UNKNOWN
property_checkert::as_string
static std::string as_string(resultt)
Definition:
property_checker.cpp:14
goto_tracet
TO_BE_DOCUMENTED.
Definition:
goto_trace.h:150
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition:
goto_program.h:415
message.h
property_checkert::resultt
resultt
Definition:
property_checker.h:32
property_checkert::property_statust::error_trace
goto_tracet error_trace
Definition:
property_checker.h:42
goto-programs
property_checker.h
Generated by
1.8.16