c_test_input_generator.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Test Input Generator for C
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
#define CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
 
#include <iosfwd>
 
#include <util/xml.h>
 
class goto_tracet;
class goto_trace_storaget;
class json_objectt;
class namespacet;
class optionst;
class ui_message_handlert;
 
class test_inputst
{
public:
  void output_plain_text(
    std::ostream &out,
    const namespacet &ns,
    const goto_tracet &goto_trace) const;
 
  json_objectt to_json(
    const namespacet &ns,
    const goto_tracet &goto_trace,
    bool print_trace) const;
 
  xmlt to_xml(
    const namespacet &ns,
    const goto_tracet &goto_trace,
    bool print_trace) const;
};
 
class c_test_input_generatort
{
public:
  c_test_input_generatort(
    ui_message_handlert &ui_message_handler,
    const optionst &options);
 
  void operator()(const goto_trace_storaget &);
 
protected:
  ui_message_handlert &ui_message_handler;
  const optionst &options;
 
  test_inputst operator()(const goto_tracet &goto_trace, const namespacet &ns);
};
 
#endif // CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H