java_single_path_symex_only_checkert Class Reference
#include <java_single_path_symex_only_checker.h>
Inheritance diagram for java_single_path_symex_only_checkert: Collaboration diagram for java_single_path_symex_only_checkert:Public Member Functions | |
| java_single_path_symex_only_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | |
| void | setup_symex (symex_bmct &symex) override |
| Public Member Functions inherited from single_path_symex_only_checkert | |
| single_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... | |
| virtual | ~single_path_symex_only_checkert ()=default |
| 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... | |
Additional Inherited Members | |
| Protected Member Functions inherited from single_path_symex_only_checkert | |
| void | equation_output (const symex_bmct &symex, const symex_target_equationt &equation) |
| virtual void | initialize_worklist () |
| Adds the initial goto-symex state as a path to the worklist. More... | |
| virtual bool | resume_path (path_storaget::patht &path) |
Continues exploring the given path using goto-symex. More... | |
| virtual bool | is_ready_to_decide (const symex_bmct &symex, const path_storaget::patht &path) |
Returns whether the given path produced by symex is ready to be checked. More... | |
| virtual bool | has_finished_exploration (const propertiest &) |
| Returns whether we should stop exploring paths. More... | |
| virtual void | update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation) |
Updates the properties from the equation and adds their property IDs to updated_properties. More... | |
| virtual void | final_update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties) |
Updates the properties after having finished exploration 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 inherited from single_path_symex_only_checkert | |
| abstract_goto_modelt & | goto_model |
| symbol_tablet | symex_symbol_table |
| namespacet | ns |
| guard_managert | guard_manager |
| std::unique_ptr< path_storaget > | worklist |
| std::chrono::duration< double > | symex_runtime |
| unwindsett | unwindset |
| Protected Attributes inherited from incremental_goto_checkert | |
| const optionst & | options |
| ui_message_handlert & | ui_message_handler |
| messaget | log |
Detailed Description
Definition at line 19 of file java_single_path_symex_only_checker.h.
Constructor & Destructor Documentation
◆ java_single_path_symex_only_checkert()
|
inline |
Definition at line 23 of file java_single_path_symex_only_checker.h.
Member Function Documentation
◆ setup_symex()
|
inlineoverridevirtual |
Reimplemented from single_path_symex_only_checkert.
Definition at line 31 of file java_single_path_symex_only_checker.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_single_path_symex_only_checker.h
