cprover
Loading...
Searching...
No Matches
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.
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.

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.
virtual bool resume_path (path_storaget::patht &path)
 Continues exploring the given path using goto-symex.
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.
virtual bool has_finished_exploration (const propertiest &)
 Returns whether we should stop exploring paths.
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.
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.
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_modeltgoto_model
symbol_tablet symex_symbol_table
namespacet ns
guard_managert guard_manager
std::unique_ptr< path_storagetworklist
std::chrono::duration< double > symex_runtime
unwindsett unwindset
Protected Attributes inherited from incremental_goto_checkert
const optionstoptions
ui_message_handlertui_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()

java_single_path_symex_only_checkert::java_single_path_symex_only_checkert ( const optionst & options,
ui_message_handlert & ui_message_handler,
abstract_goto_modelt & goto_model )
inline

Definition at line 23 of file java_single_path_symex_only_checker.h.

Member Function Documentation

◆ setup_symex()

void java_single_path_symex_only_checkert::setup_symex ( symex_bmct & 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: