goto_verifier.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto Verifier Interface
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
#define CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
 
#include "properties.h"
 
#include <util/message.h>
 
class optionst;
class ui_message_handlert;
 
class goto_verifiert
{
public:
  goto_verifiert() = delete;
  goto_verifiert(const goto_verifiert &) = delete;
  virtual ~goto_verifiert() = default;
 
  virtual resultt operator()() = 0;
 
  virtual void report() = 0;
 
  const propertiest &get_properties()
  {
    return properties;
  }
 
protected:
  goto_verifiert(const optionst &, ui_message_handlert &);
 
  const optionst &options;
  ui_message_handlert &ui_message_handler;
  messaget log;
  propertiest properties;
};
 
#endif // CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H