CBMC
smt2irep.cpp
Go to the documentation of this file.
1 
4 
6 #include <util/message.h>
7 
8 #include <sstream>
9 
11  const smt2_parser_test_resultt &left,
12  const smt2_parser_test_resultt &right)
13 {
14  return left.parsed_output == right.parsed_output &&
15  left.messages == right.messages;
16 }
17 
18 smt2_parser_test_resultt smt2irep(const std::string &input)
19 {
20  std::stringstream in_stream(input);
21  std::stringstream out_stream;
22  stream_message_handlert message_handler(out_stream);
23  return {smt2irep(in_stream, message_handler), out_stream.str()};
24 }
25 
26 std::ostream &operator<<(
27  std::ostream &output_stream,
28  const smt2_parser_test_resultt &test_result)
29 {
30  const std::string printed_irep =
31  test_result.parsed_output.has_value()
32  ? '{' + test_result.parsed_output->pretty(0, 0) + '}'
33  : "empty optional irep";
34  output_stream << '{' << printed_irep << ", \"" << test_result.messages
35  << "\"}";
36  return output_stream;
37 }
38 
40  std::string expected_error)
41  : expected_error{std::move(expected_error)}
42 {
43 }
44 
46  const smt2_parser_test_resultt &result) const
47 {
48  return !result.parsed_output.has_value() &&
49  result.messages.find(expected_error) != std::string::npos;
50 }
51 
53 {
54  return "Expecting empty parse tree and \"" + expected_error +
55  "\" printed to output.";
56 }
57 
59 {
60  return {std::move(parse_tree), ""};
61 }
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
smt2_parser_error_containingt(std::string expected_error)
Definition: smt2irep.cpp:39
bool match(const smt2_parser_test_resultt &exception) const override
Definition: smt2irep.cpp:45
std::string describe() const override
Definition: smt2irep.cpp:52
std::optional< irept > smt2irep(std::istream &in, message_handlert &message_handler)
returns an irep for an SMT-LIB2 expression read from a given stream returns {} when EOF is encountere...
Definition: smt2irep.cpp:92
std::optional< irept > parsed_output
Definition: smt2irep.h:15
std::string messages
Definition: smt2irep.h:16
bool operator==(const smt2_parser_test_resultt &left, const smt2_parser_test_resultt &right)
Author: Diffblue Ltd.
Definition: smt2irep.cpp:10
std::ostream & operator<<(std::ostream &output_stream, const smt2_parser_test_resultt &test_result)
Definition: smt2irep.cpp:26
smt2_parser_test_resultt smt2_parser_success(irept parse_tree)
Definition: smt2irep.cpp:58