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:
26 const optionst &options,
32 {
34 }
35
37 {
40 }
41
42 void report() override
43 {
45 {
46 case resultt::PASS:
48 incremental_goto_checker.output_proof();
49 break;
50
51 case resultt::FAIL:
52 {
54 goto_tracet goto_trace = incremental_goto_checker.build_shortest_trace();
56 goto_trace,
57 incremental_goto_checker.get_namespace(),
61 incremental_goto_checker.output_error_witness(goto_trace);
62 break;
63 }
64
65 case resultt::UNKNOWN:
67 break;
68
69 case resultt::ERROR:
71 break;
72 }
73 }
74
75protected:
77 incremental_goto_checkerT incremental_goto_checker;
78};
79
80#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:65
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.
Trace of a GOTO program.
Definition: goto_trace.h:175
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
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 ...
Definition: properties.cpp:260
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
Definition: properties.cpp:68
resultt
The result of goto verifying.
Definition: properties.h:45
void report_success(ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:32
void report_inconclusive(ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:88
void report_error(ui_message_handlert &ui_message_handler)
void report_failure(ui_message_handlert &ui_message_handler)
Definition: report_util.cpp:60
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:219