1
2// Copyright (C) 2008-2018 Lorenzo Caminiti
3// Distributed under the Boost Software License, Version 1.0 (see accompanying
4// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
5// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
6
7#include <vector>
8#include <limits>
9#include <cassert>
10
11//[ifdef_macro_function
12// Use macro interface to completely disable contract code compilation.
13#include <boost/contract_macro.hpp>
14
15int inc(int& x) {
16 int result;
17 BOOST_CONTRACT_OLD_PTR(int)(old_x, x);
18 BOOST_CONTRACT_FUNCTION()
19 BOOST_CONTRACT_PRECONDITION([&] {
20 BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max());
21 })
22 BOOST_CONTRACT_POSTCONDITION([&] {
23 BOOST_CONTRACT_ASSERT(x == *old_x + 1);
24 BOOST_CONTRACT_ASSERT(result == *old_x);
25 })
26 ;
27
28 return result = x++;
29}
30//]
31
32template<typename T>
33class pushable {
34 friend class boost::contract::access; // Left in code (almost no overhead).
35
36 BOOST_CONTRACT_INVARIANT({
37 BOOST_CONTRACT_ASSERT(capacity() <= max_size());
38 })
39
40public:
41 virtual void push_back(
42 T const& x,
43 boost::contract::virtual_* v = 0 // Left in code (almost no overhead).
44 ) = 0;
45
46protected:
47 virtual unsigned capacity() const = 0;
48 virtual unsigned max_size() const = 0;
49};
50
51template<typename T>
52void pushable<T>::push_back(T const& x, boost::contract::virtual_* v) {
53 BOOST_CONTRACT_OLD_PTR(unsigned)(v, old_capacity, capacity());
54 BOOST_CONTRACT_PUBLIC_FUNCTION(v, this)
55 BOOST_CONTRACT_PRECONDITION([&] {
56 BOOST_CONTRACT_ASSERT(capacity() < max_size());
57 })
58 BOOST_CONTRACT_POSTCONDITION([&] {
59 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
60 })
61 ;
62 assert(false); // Shall never execute this body.
63}
64
65//[ifdef_macro_class
66class integers
67 #define BASES public pushable<int>
68 :
69 // Left in code (almost no overhead).
70 private boost::contract::constructor_precondition<integers>,
71 BASES
72{
73 // Followings left in code (almost no overhead).
74 friend class boost::contract::access;
75
76 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
77 #undef BASES
78
79 BOOST_CONTRACT_INVARIANT({
80 BOOST_CONTRACT_ASSERT(size() <= capacity());
81 })
82
83public:
84 integers(int from, int to) :
85 BOOST_CONTRACT_CONSTRUCTOR_PRECONDITION(integers)([&] {
86 BOOST_CONTRACT_ASSERT(from <= to);
87 }),
88 vect_(to - from + 1)
89 {
90 BOOST_CONTRACT_CONSTRUCTOR(this)
91 BOOST_CONTRACT_POSTCONDITION([&] {
92 BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1));
93 })
94 ;
95
96 for(int x = from; x <= to; ++x) vect_.at(n: x - from) = x;
97 }
98
99 virtual ~integers() {
100 BOOST_CONTRACT_DESTRUCTOR(this); // Check invariants.
101 }
102
103 virtual void push_back(
104 int const& x,
105 boost::contract::virtual_* v = 0 // Left in code (almost no overhead).
106 ) /* override */ {
107 BOOST_CONTRACT_OLD_PTR(unsigned)(old_size);
108 BOOST_CONTRACT_PUBLIC_FUNCTION_OVERRIDE(override_push_back)(
109 v, &integers::push_back, obj: this, args: x)
110 BOOST_CONTRACT_PRECONDITION([&] {
111 BOOST_CONTRACT_ASSERT(size() < max_size());
112 })
113 BOOST_CONTRACT_OLD([&] {
114 old_size = BOOST_CONTRACT_OLDOF(v, size());
115 })
116 BOOST_CONTRACT_POSTCONDITION([&] {
117 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
118 })
119 BOOST_CONTRACT_EXCEPT([&] {
120 BOOST_CONTRACT_ASSERT(size() == *old_size);
121 })
122 ;
123
124 vect_.push_back(x: x);
125 }
126
127private:
128 BOOST_CONTRACT_OVERRIDE(push_back) // Left in code (almost no overhead).
129
130 /* ... */
131//]
132
133public: // Could program contracts for these too...
134 unsigned size() const { return vect_.size(); }
135 unsigned max_size() const { return vect_.max_size(); }
136 unsigned capacity() const { return vect_.capacity(); }
137
138private:
139 std::vector<int> vect_;
140};
141
142int main() {
143 integers i(1, 10);
144 int x = 123;
145 i.push_back(x: inc(x));
146 assert(x == 124);
147 assert(i.size() == 11);
148 return 0;
149}
150
151

source code of boost/libs/contract/example/features/ifdef_macro.cpp