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
6
#include <
testing-utils/use_catch.h
>
7
8
#include <
util/irep.h
>
9
#include <
util/optional.h
>
10
11
#include <string>
12
13
struct
smt2_parser_test_resultt
14
{
15
optionalt<irept>
parsed_output
;
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
25
class
smt2_parser_error_containingt
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
37
smt2_parser_test_resultt
smt2_parser_success
(
irept
parse_tree);
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
unit
testing-utils
smt2irep.h
Generated by
1.8.17