cprover
Loading...
Searching...
No Matches
stop_on_fail_verifier.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Verifier for stopping at the first failing property
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H
13#define CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H
14
15#include "bmc_util.h"
16#include "goto_verifier.h"
17
21template <class incremental_goto_checkerT>
23{
24public:
35
41
42 void report() override
43 {
45 {
46 case resultt::PASS:
49 incremental_goto_checker.output_proof();
50 break;
51
52 case resultt::FAIL:
53 {
55 goto_tracet goto_trace = incremental_goto_checker.build_shortest_trace();
57 goto_trace,
58 incremental_goto_checker.get_namespace(),
62 incremental_goto_checker.output_error_witness(goto_trace);
63 break;
64 }
65
68 break;
69
70 case resultt::ERROR:
72 break;
73 }
75 }
76
77protected:
79 incremental_goto_checkerT incremental_goto_checker;
80};
81
82#endif // CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_H
void output_error_trace(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, ui_message_handlert &ui_message_handler)
Definition bmc_util.cpp:64
void message_building_error_trace(messaget &log)
Outputs a message that an error trace is being built.
Definition bmc_util.cpp:35
Bounded Model Checking Utilities.
Abstract interface to eager or lazy GOTO models.
Trace of a GOTO program.
Definition goto_trace.h:177
An implementation of goto_verifiert checks all properties in a goto model.
propertiest properties
const optionst & options
ui_message_handlert & ui_message_handler
Stops when the first failing property is found.
void report() override
Report results.
abstract_goto_modelt & goto_model
resultt operator()() override
Check whether all properties hold.
stop_on_fail_verifiert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
incremental_goto_checkerT incremental_goto_checker
Goto Verifier 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.
resultt
The result of goto verifying.
Definition properties.h:45
@ UNKNOWN
No property was violated, neither was there an error.
@ PASS
No properties were violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
Some properties were violated.
void output_properties(const propertiest &properties, std::size_t iterations, ui_message_handlert &ui_message_handler)
void report_success(ui_message_handlert &ui_message_handler)
void report_inconclusive(ui_message_handlert &ui_message_handler)
void report_error(ui_message_handlert &ui_message_handler)
void report_failure(ui_message_handlert &ui_message_handler)
Options for printing the trace using show_goto_trace.
Definition goto_trace.h:221