cprover
c_test_input_generator.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Test Input Generator for C
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
13
15
17
18#include <util/json.h>
19#include <util/json_stream.h>
20#include <util/options.h>
21#include <util/string_utils.h>
22#include <util/symbol.h>
23#include <util/ui_message.h>
24#include <util/xml.h>
25
30
32 ui_message_handlert &ui_message_handler,
33 const optionst &options)
34 : ui_message_handler(ui_message_handler), options(options)
35{
36}
37
39 std::ostream &out,
40 const namespacet &ns,
41 const goto_tracet &goto_trace) const
42{
43 const auto input_assignments =
44 make_range(goto_trace.steps)
45 .filter([](const goto_trace_stept &step) { return step.is_input(); })
46 .map([ns](const goto_trace_stept &step) {
47 return id2string(step.io_id) + '=' +
48 from_expr(ns, step.function_id, step.io_args.front());
49 });
50 join_strings(out, input_assignments.begin(), input_assignments.end(), ", ");
51 out << '\n';
52}
53
55 const namespacet &ns,
56 const goto_tracet &goto_trace,
57 bool print_trace) const
58{
59 json_objectt json_result;
60 json_arrayt &json_inputs = json_result["inputs"].make_array();
61
62 for(const auto &step : goto_trace.steps)
63 {
64 if(step.is_input())
65 {
66 json_objectt json_input({{"id", json_stringt(step.io_id)}});
67 if(step.io_args.size() == 1)
68 json_input["value"] =
69 json(step.io_args.front(), ns, ns.lookup(step.function_id).mode);
70 json_inputs.push_back(std::move(json_input));
71 }
72 }
73
74 json_arrayt goal_refs;
75 for(const auto &goal_id : goto_trace.get_failed_property_ids())
76 {
77 goal_refs.push_back(json_stringt(goal_id));
78 }
79 json_result["coveredGoals"] = std::move(goal_refs);
80
81 if(print_trace)
82 {
83 json_arrayt json_trace;
84 convert(ns, goto_trace, json_trace);
85 json_result["trace"] = std::move(json_trace);
86 }
87 return json_result;
88}
89
91 const namespacet &ns,
92 const goto_tracet &goto_trace,
93 bool print_trace) const
94{
95 xmlt xml_result("test");
96 if(print_trace)
97 {
98 convert(ns, goto_trace, xml_result.new_element());
99 }
100 else
101 {
102 xmlt &xml_test = xml_result.new_element("inputs");
103
104 for(const auto &step : goto_trace.steps)
105 {
106 if(step.is_input())
107 {
108 xmlt &xml_input = xml_test.new_element("input");
109 xml_input.set_attribute("id", id2string(step.io_id));
110 if(step.io_args.size() == 1)
111 xml_input.new_element("value") = xml(step.io_args.front(), ns);
112 }
113 }
114 }
115
116 for(const auto &goal_id : goto_trace.get_failed_property_ids())
117 {
118 xmlt &xml_goal = xml_result.new_element("goal");
119 xml_goal.set_attribute("id", id2string(goal_id));
120 }
121
122 return xml_result;
123}
124
126operator()(const goto_tracet &goto_trace, const namespacet &ns)
127{
128 test_inputst test_inputs;
129 return test_inputs;
130}
131
133{
134 const namespacet &ns = traces.get_namespace();
135 const bool print_trace = options.get_bool_option("trace");
137 switch(ui_message_handler.get_ui())
138 {
140 log.result() << "\nTest suite:\n";
141 for(const auto &trace : traces.all())
142 {
143 test_inputst test_inputs = (*this)(trace, ns);
144 test_inputs.output_plain_text(log.result(), ns, trace);
145 }
146 log.result() << messaget::eom;
147 break;
149 {
150 if(log.status().tellp() > 0)
151 log.status() << messaget::eom; // force end of previous message
152 json_stream_objectt &json_result =
154 json_stream_arrayt &tests_array =
155 json_result.push_back_stream_array("tests");
156
157 for(const auto &trace : traces.all())
158 {
159 test_inputst test_inputs = (*this)(trace, ns);
160 tests_array.push_back(test_inputs.to_json(ns, trace, print_trace));
161 }
162 break;
163 }
165 for(const auto &trace : traces.all())
166 {
167 test_inputst test_inputs = (*this)(trace, ns);
168 log.result() << test_inputs.to_xml(ns, trace, print_trace);
169 }
170 break;
171 }
172}
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
Test Input Generator for C.
c_test_input_generatort(ui_message_handlert &ui_message_handler, const optionst &options)
ui_message_handlert & ui_message_handler
void operator()(const goto_trace_storaget &)
Extracts test inputs for all traces and outputs them.
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
irep_idt function_id
Definition: goto_trace.h:111
io_argst io_args
Definition: goto_trace.h:137
irep_idt io_id
Definition: goto_trace.h:135
bool is_input() const
Definition: goto_trace.h:64
const namespacet & get_namespace() const
const std::list< goto_tracet > & all() const
Trace of a GOTO program.
Definition: goto_trace.h:175
stepst steps
Definition: goto_trace.h:178
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
Definition: goto_trace.cpp:801
jsont & push_back(const jsont &json)
Definition: json.h:212
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
Definition: json_stream.h:106
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
json_arrayt & make_array()
Definition: json.h:420
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
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.
void output_plain_text(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace) const
Outputs the test inputs in plain text format.
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.
virtual uit get_ui() const
Definition: ui_message.h:33
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:40
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
Goto Trace Storage.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
Expressions in JSON.
Traces of GOTO Programs.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Options.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:62
Symbol table entry.
Traces of GOTO Programs.