cprover
|
Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration. More...
#include <single_loop_incremental_symex_checker.h>
Public Member Functions | |
single_loop_incremental_symex_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | |
resultt | operator() (propertiest &) override |
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold. | |
goto_tracet | build_full_trace () const override |
Builds and returns the complete trace. | |
goto_tracet | build_trace (const irep_idt &) const override |
Builds and returns the trace for the FAILed property with the given property_id . | |
goto_tracet | build_shortest_trace () const override |
Builds and returns the trace up to the first failed property. | |
const namespacet & | get_namespace () const override |
Returns the namespace associated with the traces. | |
void | output_error_witness (const goto_tracet &) override |
void | output_proof () override |
![]() | |
incremental_goto_checkert ()=delete | |
incremental_goto_checkert (const incremental_goto_checkert &)=delete | |
virtual | ~incremental_goto_checkert ()=default |
virtual void | report () |
Additional reporting that may result from the underlying solver, no-op by default. | |
![]() | |
virtual | ~goto_trace_providert ()=default |
![]() | |
virtual | ~witness_providert ()=default |
Additional Inherited Members | |
![]() | |
incremental_goto_checkert (const optionst &, ui_message_handlert &) | |
Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration.
Definition at line 31 of file single_loop_incremental_symex_checker.h.
single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert | ( | const optionst & | options, |
ui_message_handlert & | ui_message_handler, | ||
abstract_goto_modelt & | goto_model | ||
) |
Definition at line 25 of file single_loop_incremental_symex_checker.cpp.
|
overridevirtual |
Builds and returns the complete trace.
Implements goto_trace_providert.
Definition at line 193 of file single_loop_incremental_symex_checker.cpp.
|
overridevirtual |
Builds and returns the trace up to the first failed property.
Implements goto_trace_providert.
Definition at line 206 of file single_loop_incremental_symex_checker.cpp.
|
overridevirtual |
Builds and returns the trace for the FAILed property with the given property_id
.
Implements goto_trace_providert.
Definition at line 223 of file single_loop_incremental_symex_checker.cpp.
|
overridevirtual |
Returns the namespace associated with the traces.
Implements goto_trace_providert.
Definition at line 237 of file single_loop_incremental_symex_checker.cpp.
|
overridevirtual |
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert
hold.
[out] | properties | Properties updated to whether their status have been determined. Newly discovered properties are added. |
build_error_trace
before any subsequent call to operator(). incremental_goto_checkert
derivatives shall be implemented in a way such that repeated calls to operator() shall return when the next FAILed property has been found until eventually it does not find any failing properties any more. Note: This operator can handle shrinking and expanding sets of properties in repeated invocations.
Implements incremental_goto_checkert.
Definition at line 71 of file single_loop_incremental_symex_checker.cpp.
|
overridevirtual |
Implements witness_providert.
Definition at line 247 of file single_loop_incremental_symex_checker.cpp.
|
overridevirtual |
Implements witness_providert.
Definition at line 242 of file single_loop_incremental_symex_checker.cpp.
Definition at line 66 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 59 of file single_loop_incremental_symex_checker.h.
Definition at line 65 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 56 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 61 of file single_loop_incremental_symex_checker.h.
Definition at line 64 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 58 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 60 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 67 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 63 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 57 of file single_loop_incremental_symex_checker.h.
|
protected |
Definition at line 62 of file single_loop_incremental_symex_checker.h.