#include <multi_path_symex_only_checker.h>
◆ multi_path_symex_only_checkert()
◆ generate_equation()
void multi_path_symex_only_checkert::generate_equation |
( |
| ) |
|
|
protectedvirtual |
◆ operator()()
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_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.
◆ update_properties()
void multi_path_symex_only_checkert::update_properties |
( |
propertiest & |
properties, |
|
|
std::unordered_set< irep_idt > & |
updated_properties |
|
) |
| |
|
protectedvirtual |
◆ equation
◆ goto_model
◆ guard_manager
◆ ns
◆ path_storage
path_fifot multi_path_symex_only_checkert::path_storage |
|
protected |
◆ symex
◆ symex_symbol_table
◆ unwindset
unwindsett multi_path_symex_only_checkert::unwindset |
|
protected |
The documentation for this class was generated from the following files: