cprover
Loading...
Searching...
No Matches
all_properties_verifier.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Verifier for Verifying all Properties
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H
13#define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H
14
15#include "goto_verifier.h"
16
18#include "properties.h"
19#include "report_util.h"
20
21template <class incremental_goto_checkerT>
23{
24public:
26 const optionst &options,
32 {
34 }
35
37 {
38 while(incremental_goto_checker(properties).progress !=
40 {
41 // loop until we are done
42 ++iterations;
43 }
45 }
46
47 void report() override
48 {
51 }
52
53protected:
55 incremental_goto_checkerT incremental_goto_checker;
56 std::size_t iterations = 1;
57};
58
59#endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H
Abstract interface to eager or lazy GOTO models.
void report() override
Report results.
abstract_goto_modelt & goto_model
incremental_goto_checkerT incremental_goto_checker
resultt operator()() override
Check whether all properties hold.
all_properties_verifiert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
An implementation of goto_verifiert checks all properties in a goto model.
Definition: goto_verifier.h:27
propertiest properties
Definition: goto_verifier.h:56
const optionst & options
Definition: goto_verifier.h:53
ui_message_handlert & ui_message_handler
Definition: goto_verifier.h:54
Goto Verifier Interface.
Incremental Goto Checker Interface.
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
Definition: properties.cpp:260
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
Definition: properties.cpp:68
Properties.
resultt
The result of goto verifying.
Definition: properties.h:45
void output_properties(const propertiest &properties, std::size_t iterations, ui_message_handlert &ui_message_handler)
void output_overall_result(resultt result, ui_message_handlert &ui_message_handler)
Bounded Model Checking Utilities.
@ DONE
The goto checker has returned all results for the given set of properties.