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
108
|
#ifndef BOOST_CONTRACT_CONSTRUCTOR_HPP_
#define BOOST_CONTRACT_CONSTRUCTOR_HPP_
// 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
/** @file
Program contracts for constructors.
*/
#include <boost/contract/core/config.hpp>
#include <boost/contract/core/specify.hpp>
#include <boost/contract/core/access.hpp>
#include <boost/contract/core/constructor_precondition.hpp>
#if !defined(BOOST_CONTRACT_NO_CONSTRUCTORS) || \
!defined(BOOST_CONTRACT_NO_PRECONDITIONS) || \
defined(BOOST_CONTRACT_STATIC_LINK)
#include <boost/contract/detail/operation/constructor.hpp>
#endif
namespace boost { namespace contract {
/**
Program contracts for constructors.
This is used to specify postconditions, exception guarantees, old value copies
at body, and check class invariants for constructors (see
@RefClass{boost::contract::constructor_precondition} to specify preconditions
for constructors instead):
@code
class u {
friend class boost::contract:access;
void invariant() const { // Optional (as for static and volatile).
BOOST_CONTRACT_ASSERT(...);
...
}
public:
u(...) {
boost::contract::old_ptr<old_type> old_var;
boost::contract::check c = boost::contract::constructor(this)
// No `.precondition` (use `constructor_precondition` if needed).
.old([&] { // Optional.
old_var = BOOST_CONTRACT_OLDOF(old_expr);
...
})
.postcondition([&] { // Optional.
BOOST_CONTRACT_ASSERT(...);
...
})
.except([&] { // Optional.
BOOST_CONTRACT_ASSERT(...);
...
})
;
... // Constructor body.
}
...
};
@endcode
For optimization, this can be omitted for constructors that do not have
postconditions and exception guarantees, within classes that have no invariants.
@see @RefSect{tutorial.constructors, Constructors}
@param obj The object @c this from the scope of the enclosing constructor
declaring the contract.
(Constructors check all class invariants, including static and
volatile invariants, see @RefSect{tutorial.class_invariants,
Class Invariants} and
@RefSect{extras.volatile_public_functions,
Volatile Public Functions}).
@tparam Class The type of the class containing the constructor declaring the
contract.
(Usually this template parameter is automatically deduced by C++
and it does not need to be explicitly specified by programmers.)
@return The result of this function must be explicitly assigned to a variable of
type @RefClass{boost::contract::check} declared locally just before the
code of the constructor body (otherwise this library will generate a
run-time error, see @RefMacro{BOOST_CONTRACT_ON_MISSING_CHECK_DECL}).
*/
template<class Class>
specify_old_postcondition_except<> constructor(Class* obj) {
// Must #if also on ..._PRECONDITIONS here because specify_... is generic.
#if !defined(BOOST_CONTRACT_NO_CONSTRUCTORS) || \
!defined(BOOST_CONTRACT_NO_PRECONDITIONS) || \
defined(BOOST_CONTRACT_STATIC_LINK)
return specify_old_postcondition_except<>(
new boost::contract::detail::constructor<Class>(obj));
#else
return specify_old_postcondition_except<>();
#endif
}
} } // namespace
#endif // #include guard
|
