cprover
Loading...
Searching...
No Matches
all_properties_verifier_with_trace_storage.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Verifier for Verifying all Properties that stores Traces
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H
13#define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H
14
15#include "goto_verifier.h"
16
17#include "bmc_util.h"
18#include "goto_trace_storage.h"
20#include "properties.h"
21#include "report_util.h"
22
23template <class incremental_goto_checkerT>
25{
26public:
38
40 {
41 while(true)
42 {
43 const auto result = incremental_goto_checker(properties);
45 break;
46
47 // we've got an error trace
48 if(options.get_bool_option("trace"))
49 {
51 for(const auto &property_id : result.updated_properties)
52 {
53 if(properties.at(property_id).status == property_statust::FAIL)
54 {
55 // get correctly truncated error trace for property and store it
57 incremental_goto_checker.build_trace(property_id));
58 }
59 }
60 }
61
62 ++iterations;
63 }
64
66 }
67
83
85 {
86 return traces;
87 }
88
89protected:
92 std::size_t iterations = 1;
94};
95
96#endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H
void message_building_error_trace(messaget &log)
Outputs a message that an error trace is being built.
Definition bmc_util.cpp:36
Bounded Model Checking Utilities.
Abstract interface to eager or lazy GOTO models.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
all_properties_verifier_with_trace_storaget(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
resultt operator()() override
Check whether all properties hold.
const goto_tracet & insert(goto_tracet &&)
Store trace that ends in a violated assertion.
An implementation of goto_verifiert checks all properties in a goto model.
propertiest properties
const optionst & options
ui_message_handlert & ui_message_handler
bool get_bool_option(const std::string &option) const
Definition options.cpp:44
Goto Trace Storage.
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 ...
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
Properties.
@ FAIL
The property was violated.
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)
void output_properties_with_traces(const propertiest &properties, const goto_trace_storaget &traces, const trace_optionst &trace_options, std::size_t iterations, ui_message_handlert &ui_message_handler)
Bounded Model Checking Utilities.
@ DONE
The goto checker has returned all results for the given set of properties.
Options for printing the trace using show_goto_trace.
Definition goto_trace.h:219