CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
multi_path_symex_only_checkert Class Reference

#include <multi_path_symex_only_checker.h>

+ Inheritance diagram for multi_path_symex_only_checkert:
[フレーム]
[legend]
+ Collaboration diagram for multi_path_symex_only_checkert:
[フレーム]
[legend]

Public Member Functions

  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.
 

Protected Member Functions

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

abstract_goto_modelt &  goto_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 optionst &  options
 
ui_message_handlert &  ui_message_handler
 
messaget  log
 

Detailed Description

Definition at line 22 of file multi_path_symex_only_checker.h.

Constructor & Destructor Documentation

◆  multi_path_symex_only_checkert()

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

Definition at line 22 of file multi_path_symex_only_checker.cpp.

Member Function Documentation

◆  generate_equation()

void multi_path_symex_only_checkert::generate_equation ( )
protectedvirtual

Generates the equation by running goto-symex.

Definition at line 75 of file multi_path_symex_only_checker.cpp.

◆  operator()()

incremental_goto_checkert::resultt multi_path_symex_only_checkert::operator() ( propertiest &  properties )
overridevirtual

Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold.

Parameters
[out] properties Properties updated to whether their status have been determined. Newly discovered properties are added.
Returns
whether the goto checker found a violated property (FOUND_FAIL) or whether it is DONE with the given properties, together with the properties whose status changed since the last call to operator(). After returning DONE, another call to operator() with the same properties will return DONE and leave the properties' status unchanged. If there is a property with status FAIL then its counterexample can be retrieved by calling build_error_trace before any subsequent call to operator(). incremental_goto_checkert derivatives shall be implemented in a way such that repeated calls to operator() shall return when the next FAILed property has been found until eventually it does not find any failing properties any more.

Implements incremental_goto_checkert.

Definition at line 44 of file multi_path_symex_only_checker.cpp.

◆  update_properties()

void multi_path_symex_only_checkert::update_properties ( propertiest &  properties,
std::unordered_set< irep_idt > &  updated_properties 
)
protectedvirtual

Updates the properties from the equation and adds their property IDs to updated_properties.

Definition at line 95 of file multi_path_symex_only_checker.cpp.

Member Data Documentation

◆  equation

symex_target_equationt multi_path_symex_only_checkert::equation
protected

Definition at line 36 of file multi_path_symex_only_checker.h.

◆  goto_model

abstract_goto_modelt& multi_path_symex_only_checkert::goto_model
protected

Definition at line 33 of file multi_path_symex_only_checker.h.

◆  guard_manager

guard_managert multi_path_symex_only_checkert::guard_manager
protected

Definition at line 37 of file multi_path_symex_only_checker.h.

◆  ns

namespacet multi_path_symex_only_checkert::ns
protected

Definition at line 35 of file multi_path_symex_only_checker.h.

◆  path_storage

path_fifot multi_path_symex_only_checkert::path_storage
protected

Definition at line 38 of file multi_path_symex_only_checker.h.

◆  symex

symex_bmct multi_path_symex_only_checkert::symex
protected

Definition at line 40 of file multi_path_symex_only_checker.h.

◆  symex_symbol_table

symbol_tablet multi_path_symex_only_checkert::symex_symbol_table
protected

Definition at line 34 of file multi_path_symex_only_checker.h.

◆  unwindset

unwindsett multi_path_symex_only_checkert::unwindset
protected

Definition at line 39 of file multi_path_symex_only_checker.h.

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

AltStyle によって変換されたページ (->オリジナル) /