cprover
Loading...
Searching...
No Matches
stop_on_fail_verifier_with_fault_localization.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Verifier for stopping at the first failing property
4 and localizing the fault
5
6Author: Daniel Kroening, Peter Schrammel
7
8\*******************************************************************/
9
13
14#ifndef CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_WITH_FAULT_LOCALIZATION_H
15#define CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_WITH_FAULT_LOCALIZATION_H
16
17#include "bmc_util.h"
19#include "goto_verifier.h"
20
24template <class incremental_goto_checkerT>
26{
27public:
29 const optionst &options,
35 {
37 }
38
40 {
43 }
44
45 void report() override
46 {
48 {
49 case resultt::PASS:
51 break;
52
53 case resultt::FAIL:
54 {
55 const goto_tracet goto_trace =
56 incremental_goto_checker.build_shortest_trace();
57 const fault_location_infot fault_location =
58 incremental_goto_checker.localize_fault(
59 goto_trace.get_last_step().property_id);
60
62 goto_trace,
63 incremental_goto_checker.get_namespace(),
65 fault_location,
67
69 break;
70 }
71
72 case resultt::UNKNOWN:
74 break;
75
76 case resultt::ERROR:
78 break;
79 }
80 }
81
82protected:
84 incremental_goto_checkerT incremental_goto_checker;
85};
86
87#endif // CPROVER_GOTO_CHECKER_STOP_ON_FAIL_VERIFIER_WITH_FAULT_LOCALIZATION_H
Bounded Model Checking Utilities.
Abstract interface to eager or lazy GOTO models.
irep_idt property_id
Definition: goto_trace.h:122
Trace of a GOTO program.
Definition: goto_trace.h:175
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Definition: goto_trace.h:203
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 and localizes the fault Requires an incremental goto c...
resultt operator()() override
Check whether all properties hold.
stop_on_fail_verifier_with_fault_localizationt(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Interface for Goto Checkers to provide Fault Localization.
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 output_error_trace_with_fault_localization(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, const fault_location_infot &fault_location_info, ui_message_handlert &ui_message_handler)
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