CBMC
smt2irep.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_TESTING_UTILS_SMT2IREP_H
4 #define CPROVER_TESTING_UTILS_SMT2IREP_H
5 
7 
8 #include <util/irep.h>
9 #include <util/optional.h>
10 
11 #include <string>
12 
14 {
16  std::string messages;
17 };
18 
19 bool operator==(
20  const smt2_parser_test_resultt &left,
21  const smt2_parser_test_resultt &right);
22 
23 smt2_parser_test_resultt smt2irep(const std::string &input);
24 
26  : public Catch::MatcherBase<smt2_parser_test_resultt>
27 {
28 public:
29  explicit smt2_parser_error_containingt(std::string expected_error);
30  bool match(const smt2_parser_test_resultt &exception) const override;
31  std::string describe() const override;
32 
33 private:
34  std::string expected_error;
35 };
36 
38 
39 #endif // CPROVER_TESTING_UTILS_SMT2IREP_H
optional.h
smt2_parser_error_containingt
Definition: smt2irep.h:25
smt2_parser_error_containingt::describe
std::string describe() const override
Definition: smt2irep.cpp:52
operator==
bool operator==(const smt2_parser_test_resultt &left, const smt2_parser_test_resultt &right)
Author: Diffblue Ltd.
Definition: smt2irep.cpp:10
smt2_parser_error_containingt::expected_error
std::string expected_error
Definition: smt2irep.h:34
smt2_parser_test_resultt::parsed_output
optionalt< irept > parsed_output
Definition: smt2irep.h:15
smt2irep
optionalt< irept > smt2irep(std::istream &, message_handlert &)
returns an irep for an SMT-LIB2 expression read from a given stream returns {} when EOF is encountere...
Definition: smt2irep.cpp:91
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
smt2_parser_error_containingt::match
bool match(const smt2_parser_test_resultt &exception) const override
Definition: smt2irep.cpp:45
smt2_parser_test_resultt::messages
std::string messages
Definition: smt2irep.h:16
smt2_parser_test_resultt
Definition: smt2irep.h:13
smt2_parser_error_containingt::smt2_parser_error_containingt
smt2_parser_error_containingt(std::string expected_error)
Definition: smt2irep.cpp:39
use_catch.h
smt2_parser_success
smt2_parser_test_resultt smt2_parser_success(irept parse_tree)
Definition: smt2irep.cpp:58
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
irep.h