CBMC
|
#include <multi_path_symex_only_checker.h>
Public Member Functions | |
multi_path_symex_only_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... | |
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... | |
Protected Member Functions | |
virtual void | generate_equation () |
Generates the equation by running goto-symex. More... | |
virtual void | update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties) |
Updates the properties from the equation and adds their property IDs to updated_properties . More... | |
Protected Member Functions inherited from incremental_goto_checkert | |
incremental_goto_checkert (const optionst &, ui_message_handlert &) | |
Protected Attributes | |
abstract_goto_modelt & | goto_model |
symbol_tablet | symex_symbol_table |
namespacet | ns |
symex_target_equationt | equation |
guard_managert | guard_manager |
path_fifot | path_storage |
unwindsett | unwindset |
symex_bmct | symex |
Protected Attributes inherited from incremental_goto_checkert | |
const optionst & | options |
ui_message_handlert & | ui_message_handler |
messaget | log |
Definition at line 23 of file multi_path_symex_only_checker.h.
multi_path_symex_only_checkert::multi_path_symex_only_checkert | ( | const optionst & | options, |
ui_message_handlert & | ui_message_handler, | ||
abstract_goto_modelt & | goto_model | ||
) |
Definition at line 22 of file multi_path_symex_only_checker.cpp.
|
protectedvirtual |
Generates the equation by running goto-symex.
Definition at line 74 of file multi_path_symex_only_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. Implements incremental_goto_checkert.
Definition at line 43 of file multi_path_symex_only_checker.cpp.
|
protectedvirtual |
Updates the properties
from the equation
and adds their property IDs to updated_properties
.
Definition at line 94 of file multi_path_symex_only_checker.cpp.
|
protected |
Definition at line 37 of file multi_path_symex_only_checker.h.
|
protected |
Definition at line 34 of file multi_path_symex_only_checker.h.
|
protected |
Definition at line 38 of file multi_path_symex_only_checker.h.
|
protected |
Definition at line 36 of file multi_path_symex_only_checker.h.
|
protected |
Definition at line 39 of file multi_path_symex_only_checker.h.
|
protected |
Definition at line 41 of file multi_path_symex_only_checker.h.
|
protected |
Definition at line 35 of file multi_path_symex_only_checker.h.
|
protected |
Definition at line 40 of file multi_path_symex_only_checker.h.