CBMC
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 namespacetget_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_decidertproperty_decider
 
- 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_checker.h.

Constructor & Destructor Documentation

◆ java_single_path_symex_checkert()

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

Definition at line 22 of file java_single_path_symex_checker.h.

Member Function Documentation

◆ build_full_trace()

goto_tracet java_single_path_symex_checkert::build_full_trace ( ) const
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()

goto_tracet java_single_path_symex_checkert::build_shortest_trace ( ) const
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()

goto_tracet java_single_path_symex_checkert::build_trace ( const irep_idt property_id) const
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()

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