CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
6#include <util/irep.h>
7
9
10#include <optional>
11#include <string>
12
14{
15 std::optional<irept> parsed_output;
16 std::string messages;
17};
18
19bool operator==(
20 const smt2_parser_test_resultt &left,
21 const smt2_parser_test_resultt &right);
22
23smt2_parser_test_resultt smt2irep(const std::string &input);
24
26 : public Catch::MatcherBase<smt2_parser_test_resultt>
27{
28public:
30 bool match(const smt2_parser_test_resultt &exception) const override;
31 std::string describe() const override;
32
33private:
34 std::string expected_error;
35};
36
38
39#endif // CPROVER_TESTING_UTILS_SMT2IREP_H
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
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 &, message_handlert &)
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
smt2_parser_test_resultt smt2_parser_success(irept parse_tree)
Definition smt2irep.cpp:58