CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
smt2irep.cpp
Go to the documentation of this file.
1
2
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
18smt2_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
26std::ostream &operator<<(
27 std::ostream &output_stream,
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
STL namespace.
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
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