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>
Inheritance diagram for single_loop_incremental_symex_checkert: Collaboration diagram for single_loop_incremental_symex_checkert: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. More... | |
| goto_tracet | build_full_trace () const override |
| Builds and returns the complete trace. More... | |
| goto_tracet | build_trace (const irep_idt &) const override |
Builds and returns the trace for the FAILed property with the given property_id. More... | |
| goto_tracet | build_shortest_trace () const override |
| Builds and returns the trace up to the first failed property. More... | |
| const namespacet & | get_namespace () const override |
| Returns the namespace associated with the traces. More... | |
| void | output_error_witness (const goto_tracet &) override |
| void | output_proof () override |
| Public Member Functions inherited from incremental_goto_checkert | |
| 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. More... | |
| Public Member Functions inherited from goto_trace_providert | |
| virtual | ~goto_trace_providert ()=default |
| Public Member Functions inherited from witness_providert | |
| virtual | ~witness_providert ()=default |
Protected Attributes | |
| abstract_goto_modelt & | goto_model |
| symbol_tablet | symex_symbol_table |
| namespacet | ns |
| symex_target_equationt | equation |
| path_fifot | path_storage |
| guard_managert | guard_manager |
| unwindsett | unwindset |
| symex_bmc_incremental_one_loopt | symex |
| bool | initial_equation_generated = false |
| bool | full_equation_generated = false |
| bool | current_equation_converted = false |
| goto_symex_property_decidert | property_decider |
| Protected Attributes inherited from incremental_goto_checkert | |
| const optionst & | options |
| ui_message_handlert & | ui_message_handler |
| messaget | log |
Additional Inherited Members | |
| Protected Member Functions inherited from incremental_goto_checkert | |
| incremental_goto_checkert (const optionst &, ui_message_handlert &) | |
Detailed Description
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.
Constructor & Destructor Documentation
◆ single_loop_incremental_symex_checkert()
| 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.
Member Function Documentation
◆ build_full_trace()
|
overridevirtual |
Builds and returns the complete trace.
- Note
- If slicing is used then the trace will not be complete. E.g. with simple-slice it will end at the last assertion.
Implements goto_trace_providert.
Definition at line 193 of file single_loop_incremental_symex_checker.cpp.
◆ build_shortest_trace()
|
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.
◆ build_trace()
|
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.
◆ get_namespace()
|
overridevirtual |
Returns the namespace associated with the traces.
Implements goto_trace_providert.
Definition at line 237 of file single_loop_incremental_symex_checker.cpp.
◆ operator()()
|
overridevirtual |
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold.
- Parameters
-
[out] properties Properties updated to whether their status have been determined. Newly discovered properties are added.
- Returns
- whether the goto checker found a violated property (FOUND_FAIL) or whether it is DONE with the given properties, together with the properties whose status changed since the last call to operator(). After returning DONE, another call to operator() with the same properties will return DONE and leave the properties' status unchanged. If there is a property with status FAIL then its counterexample can be retrieved by calling
build_error_tracebefore any subsequent call to operator().incremental_goto_checkertderivatives 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 72 of file single_loop_incremental_symex_checker.cpp.
◆ output_error_witness()
|
overridevirtual |
Implements witness_providert.
Definition at line 247 of file single_loop_incremental_symex_checker.cpp.
◆ output_proof()
|
overridevirtual |
Implements witness_providert.
Definition at line 242 of file single_loop_incremental_symex_checker.cpp.
Member Data Documentation
◆ current_equation_converted
|
protected |
Definition at line 66 of file single_loop_incremental_symex_checker.h.
◆ equation
|
protected |
Definition at line 59 of file single_loop_incremental_symex_checker.h.
◆ full_equation_generated
|
protected |
Definition at line 65 of file single_loop_incremental_symex_checker.h.
◆ goto_model
|
protected |
Definition at line 56 of file single_loop_incremental_symex_checker.h.
◆ guard_manager
|
protected |
Definition at line 61 of file single_loop_incremental_symex_checker.h.
◆ initial_equation_generated
|
protected |
Definition at line 64 of file single_loop_incremental_symex_checker.h.
◆ ns
|
protected |
Definition at line 58 of file single_loop_incremental_symex_checker.h.
◆ path_storage
|
protected |
Definition at line 60 of file single_loop_incremental_symex_checker.h.
◆ property_decider
|
protected |
Definition at line 67 of file single_loop_incremental_symex_checker.h.
◆ symex
|
protected |
Definition at line 63 of file single_loop_incremental_symex_checker.h.
◆ symex_symbol_table
|
protected |
Definition at line 57 of file single_loop_incremental_symex_checker.h.
◆ unwindset
|
protected |
Definition at line 62 of file single_loop_incremental_symex_checker.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-checker/single_loop_incremental_symex_checker.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-checker/single_loop_incremental_symex_checker.cpp
