java_single_path_symex_checkert Class Reference
#include <java_single_path_symex_checker.h>
Inheritance diagram for java_single_path_symex_checkert: Collaboration diagram for java_single_path_symex_checkert:Public Member Functions | |
| java_single_path_symex_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | |
| void | setup_symex (symex_bmct &symex) override |
| goto_tracet | build_full_trace () const override |
| Builds and returns the complete trace. More... | |
| goto_tracet | build_shortest_trace () const override |
| Builds and returns the trace up to the first failed property. More... | |
| goto_tracet | build_trace (const irep_idt &property_id) const override |
Builds and returns the trace for the FAILed property with the given property_id. More... | |
| Public Member Functions inherited from single_path_symex_checkert | |
| single_path_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... | |
| 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 |
| virtual | ~single_path_symex_checkert ()=default |
| 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... | |
| Public Member Functions inherited from witness_providert | |
| virtual | ~witness_providert ()=default |
| Public Member Functions inherited from goto_trace_providert | |
| virtual | ~goto_trace_providert ()=default |
Additional Inherited Members | |
| Protected Member Functions inherited from single_path_symex_checkert | |
| bool | is_ready_to_decide (const symex_bmct &, const path_storaget::patht &) override |
Returns whether the given path produced by symex is ready to be checked. More... | |
| virtual std::chrono::duration< double > | prepare_property_decider (propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider) |
Prepare the property_decider for solving. More... | |
| virtual void | run_property_decider (incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, std::chrono::duration< double > solver_runtime) |
Run the property_decider, which calls the SAT solver, and set the status of checked properties accordingly. More... | |
| 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 | 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_checkert | |
| bool | symex_initialized = false |
| std::unique_ptr< goto_symex_property_decidert > | property_decider |
| 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_checker.h.
Constructor & Destructor Documentation
◆ java_single_path_symex_checkert()
|
inline |
Definition at line 22 of file java_single_path_symex_checker.h.
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.
Reimplemented from single_path_symex_checkert.
Definition at line 12 of file java_single_path_symex_checker.cpp.
◆ build_shortest_trace()
|
overridevirtual |
Builds and returns the trace up to the first failed property.
Reimplemented from single_path_symex_checkert.
Definition at line 20 of file java_single_path_symex_checker.cpp.
◆ build_trace()
|
overridevirtual |
Builds and returns the trace for the FAILed property with the given property_id.
Reimplemented from single_path_symex_checkert.
Definition at line 29 of file java_single_path_symex_checker.cpp.
◆ setup_symex()
|
inlineoverridevirtual |
Reimplemented from single_path_symex_only_checkert.
Definition at line 30 of file java_single_path_symex_checker.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_single_path_symex_checker.h
- /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_single_path_symex_checker.cpp
