1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
// Copyright (C) 2008-2018 Lorenzo Caminiti
// Distributed under the Boost Software License, Version 1.0 (see accompanying
// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
// Test friend functions (also forcing them to check invariants).
#include "../detail/oteststream.hpp"
#include <boost/contract/public_function.hpp>
#include <boost/contract/function.hpp>
#include <boost/contract/check.hpp>
#include <boost/contract/assert.hpp>
#include <boost/detail/lightweight_test.hpp>
#include <sstream>
boost::contract::test::detail::oteststream out;
class y;
class z;
class x {
public:
void invariant() const {
out << "x::inv" << std::endl;
BOOST_CONTRACT_ASSERT(get() >= 0);
}
x() : value_(0) {}
int get() const { return value_; }
friend void f(x&, y&, int value);
private:
int value_;
};
class y {
public:
void invariant() const {
out << "y::inv" << std::endl;
BOOST_CONTRACT_ASSERT(get() >= 0);
}
y() : value_(0) {}
int get() const { return value_; }
friend void f(x&, y&, int value);
private:
int value_;
};
void f(x& a, y& b, int value) {
boost::contract::check post = boost::contract::function()
.postcondition([&] {
out << "f::post" << std::endl;
BOOST_CONTRACT_ASSERT(a.get() == value);
BOOST_CONTRACT_ASSERT(b.get() == value);
})
;
boost::contract::check inv_b = boost::contract::public_function(&b);
boost::contract::check inv_a = boost::contract::public_function(&a);
boost::contract::check pre = boost::contract::function()
.precondition([&] {
out << "f::pre" << std::endl;
BOOST_CONTRACT_ASSERT(value > 0);
})
;
out << "f::body" << std::endl;
a.value_ = b.value_ = value;
}
int main() {
std::ostringstream ok;
x a;
y b;
out.str("");
f(a, b, 123);
ok.str(""); ok
#ifndef BOOST_CONTRACT_NO_ENTRY_INVARIANTS
<< "y::inv" << std::endl
<< "x::inv" << std::endl
#endif
#ifndef BOOST_CONTRACT_NO_PRECONDITIONS
<< "f::pre" << std::endl
#endif
<< "f::body" << std::endl
#ifndef BOOST_CONTRACT_NO_EXIT_INVARIANTS
<< "x::inv" << std::endl
<< "y::inv" << std::endl
#endif
#ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
<< "f::post" << std::endl
#endif
;
BOOST_TEST(out.eq(ok.str()));
BOOST_TEST_EQ(a.get(), 123);
BOOST_TEST_EQ(b.get(), 123);
return boost::report_errors();
}
|
