cprover
Loading...
Searching...
No Matches
java_multi_path_symex_only_checkert Class Reference

#include <java_multi_path_symex_only_checker.h>

Inheritance diagram for java_multi_path_symex_only_checkert:
Collaboration diagram for java_multi_path_symex_only_checkert:

Public Member Functions

 java_multi_path_symex_only_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Public Member Functions inherited from multi_path_symex_only_checkert
 multi_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.
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 multi_path_symex_only_checkert
virtual void generate_equation ()
 Generates the equation by running goto-symex.
virtual void update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
 Updates the properties from the equation 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 multi_path_symex_only_checkert
abstract_goto_modeltgoto_model
symbol_tablet symex_symbol_table
namespacet ns
symex_target_equationt equation
guard_managert guard_manager
path_fifot path_storage
unwindsett unwindset
symex_bmct symex
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_multi_path_symex_only_checker.h.

Constructor & Destructor Documentation

◆ java_multi_path_symex_only_checkert()

java_multi_path_symex_only_checkert::java_multi_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_multi_path_symex_only_checker.h.


The documentation for this class was generated from the following file: