cprover
stop_on_fail_verifier.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Verifier for stopping at the first failing property
4 
5 Author: 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 
21 template <class incremental_goto_checkerT>
23 {
24 public:
26  const optionst &options,
32  {
34  }
35 
36  resultt operator()() override
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 
75 protected:
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
@ 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 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