cprover
c_test_input_generator.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Test Input Generator for C
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
13 #define CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
14 
15 #include <iosfwd>
16 
17 #include <util/ui_message.h>
18 
19 class goto_tracet;
21 class json_objectt;
22 class namespacet;
23 class optionst;
24 
26 {
27 public:
29  void output_plain_text(
30  std::ostream &out,
31  const namespacet &ns,
32  const goto_tracet &goto_trace) const;
33 
37  const namespacet &ns,
38  const goto_tracet &goto_trace,
39  bool print_trace) const;
40 
43  xmlt to_xml(
44  const namespacet &ns,
45  const goto_tracet &goto_trace,
46  bool print_trace) const;
47 };
48 
50 {
51 public:
54  const optionst &options);
55 
57  void operator()(const goto_trace_storaget &);
58 
59 protected:
61  const optionst &options;
62 
64  test_inputst operator()(const goto_tracet &goto_trace, const namespacet &ns);
65 };
66 
67 #endif // CPROVER_CBMC_C_TEST_INPUT_GENERATOR_H
ui_message_handlert
Definition: ui_message.h:20
optionst
Definition: options.h:23
json_objectt
Definition: json.h:300
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
c_test_input_generatort
Definition: c_test_input_generator.h:50
c_test_input_generatort::c_test_input_generatort
c_test_input_generatort(ui_message_handlert &ui_message_handler, const optionst &options)
Definition: c_test_input_generator.cpp:30
test_inputst::to_xml
xmlt to_xml(const namespacet &ns, const goto_tracet &goto_trace, bool print_trace) const
Returns the test inputs in XML format including the trace if desired.
Definition: c_test_input_generator.cpp:89
c_test_input_generatort::operator()
void operator()(const goto_trace_storaget &)
Extracts test inputs for all traces and outputs them.
Definition: c_test_input_generator.cpp:131
xmlt
Definition: xml.h:21
test_inputst::to_json
json_objectt to_json(const namespacet &ns, const goto_tracet &goto_trace, bool print_trace) const
Returns the test inputs in JSON format including the trace if desired.
Definition: c_test_input_generator.cpp:53
c_test_input_generatort::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: c_test_input_generator.h:60
goto_trace_storaget
Definition: goto_trace_storage.h:18
test_inputst
Definition: c_test_input_generator.h:26
test_inputst::output_plain_text
void output_plain_text(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace) const
Outputs the test inputs in plain text format.
Definition: c_test_input_generator.cpp:37
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
c_test_input_generatort::options
const optionst & options
Definition: c_test_input_generator.h:61
ui_message.h