goto_harness_generator.h

Go to the documentation of this file.

/******************************************************************\
 
Module: goto_harness_generator
 
Author: Diffblue Ltd.
 
\******************************************************************/
 
#ifndef CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H
#define CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H
 
#include <list>
#include <string>
 
#include <util/irep.h>
 
class goto_modelt;
 
// NOLINTNEXTLINE(readability/namespace)
namespace harness_options_parser
{
std::string require_exactly_one_value(
  const std::string &option,
  const std::list<std::string> &values);

void assert_no_values(
  const std::string &option,
  const std::list<std::string> &values);

std::size_t require_one_size_value(
  const std::string &option,
  const std::list<std::string> &values);
// NOLINTNEXTLINE(readability/namespace)
} // namespace harness_options_parser
 
class goto_harness_generatort
{
public:
  virtual void
  generate(goto_modelt &goto_model, const irep_idt &harness_function_name) = 0;
 
  virtual ~goto_harness_generatort() = default;
  friend class goto_harness_generator_factoryt;
 
protected:
  virtual void handle_option(
    const std::string &option,
    const std::list<std::string> &values) = 0;

  virtual void validate_options(const goto_modelt &goto_model) = 0;
};
 
#endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H