abstract_goto_model.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Abstract GOTO Model
 
Author: Diffblue Ltd.
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_PROGRAMS_ABSTRACT_GOTO_MODEL_H
#define CPROVER_GOTO_PROGRAMS_ABSTRACT_GOTO_MODEL_H
 
#include "goto_functions.h"
#include "validate_goto_model.h"
 
class symbol_tablet;

class abstract_goto_modelt
{
public:
  virtual ~abstract_goto_modelt()
  {
  }

  virtual bool can_produce_function(const irep_idt &id) const = 0;

  virtual const goto_functionst::goto_functiont &get_goto_function(
    const irep_idt &id) = 0;

  virtual const goto_functionst &get_goto_functions() const = 0;

  virtual const symbol_tablet &get_symbol_table() const = 0;

  // virtual void validate(const validation_modet vm) const = 0;
  virtual void validate(
    const validation_modet vm,
    const goto_model_validation_optionst &goto_model_validation_options)
    const = 0;
};
 
#endif