single_path_symex_only_checker.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto Checker using Single Path Symbolic Execution only
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
#define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
 
#include <goto-programs/unwindset.h>
 
#include <goto-symex/path_storage.h>
 
#include "incremental_goto_checker.h"
 
#include <chrono> // IWYU pragma: keep
 
class symex_bmct;

class single_path_symex_only_checkert : public incremental_goto_checkert
{
public:
  single_path_symex_only_checkert(
    const optionst &options,
    ui_message_handlert &ui_message_handler,
    abstract_goto_modelt &goto_model);
 
  resultt operator()(propertiest &) override;
 
  virtual ~single_path_symex_only_checkert() = default;
 
protected:
  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;
 
  void equation_output(
    const symex_bmct &symex,
    const symex_target_equationt &equation);
 
  virtual void setup_symex(symex_bmct &symex)
  {
    // deriving classes may do extra work here
  }

  virtual void initialize_worklist();

  virtual bool resume_path(path_storaget::patht &path);

  virtual bool
  is_ready_to_decide(const symex_bmct &symex, const path_storaget::patht &path);

  virtual bool has_finished_exploration(const propertiest &);

  virtual void update_properties(
    propertiest &properties,
    std::unordered_set<irep_idt> &updated_properties,
    const symex_target_equationt &equation);

  virtual void final_update_properties(
    propertiest &properties,
    std::unordered_set<irep_idt> &updated_properties);
};
 
#endif // CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H