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 <boost/contract.hpp> 8 #include <vector> 9 #include <utility> 10 #include <cassert> 11 12 //[move 13 class circular_buffer : 14 private boost::contract::constructor_precondition<circular_buffer> { 15 public: invariant() const16 void invariant() const { 17 if(!moved()) { // Do not check (some) invariants for moved-from objects. 18 BOOST_CONTRACT_ASSERT(index() < size()); 19 } 20 // More invariants here that hold also for moved-from objects (e.g., 21 // all assertions necessary to successfully destroy moved-from objects). 22 } 23 24 // Move constructor. circular_buffer(circular_buffer && other)25 circular_buffer(circular_buffer&& other) : 26 boost::contract::constructor_precondition<circular_buffer>([&] { 27 BOOST_CONTRACT_ASSERT(!other.moved()); 28 }) 29 { 30 boost::contract::check c = boost::contract::constructor(this) __anon0c4c93340202null31 .postcondition([&] { 32 BOOST_CONTRACT_ASSERT(!moved()); 33 BOOST_CONTRACT_ASSERT(other.moved()); 34 }) 35 ; 36 37 move(std::forward<circular_buffer>(other)); 38 } 39 40 // Move assignment. operator =(circular_buffer && other)41 circular_buffer& operator=(circular_buffer&& other) { 42 // Moved-from can be (move) assigned (so no pre `!moved()` here). 43 boost::contract::check c = boost::contract::public_function(this) 44 .precondition([&] { 45 BOOST_CONTRACT_ASSERT(!other.moved()); 46 }) 47 .postcondition([&] { 48 BOOST_CONTRACT_ASSERT(!moved()); 49 BOOST_CONTRACT_ASSERT(other.moved()); 50 }) 51 ; 52 53 return move(std::forward<circular_buffer>(other)); 54 } 55 ~circular_buffer()56 ~circular_buffer() { 57 // Moved-from can always be destroyed (in fact no preconditions). 58 boost::contract::check c = boost::contract::destructor(this); 59 } 60 moved() const61 bool moved() const { 62 boost::contract::check c = boost::contract::public_function(this); 63 return moved_; 64 } 65 66 private: 67 bool moved_; 68 69 /* ... */ 70 //] 71 72 public: circular_buffer(std::vector<char> const & data,unsigned start=0)73 explicit circular_buffer(std::vector<char> const& data, 74 unsigned start = 0) : 75 boost::contract::constructor_precondition<circular_buffer>([&] { 76 BOOST_CONTRACT_ASSERT(start < data.size()); 77 }), 78 moved_(false), 79 data_(data), 80 index_(start) 81 { 82 boost::contract::check c = boost::contract::constructor(this) __anon0c4c93340602null83 .postcondition([&] { 84 BOOST_CONTRACT_ASSERT(!moved()); 85 }) 86 ; 87 } 88 89 // Copy constructor. circular_buffer(circular_buffer const & other)90 circular_buffer(circular_buffer const& other) : 91 boost::contract::constructor_precondition<circular_buffer>([&] { 92 BOOST_CONTRACT_ASSERT(!other.moved()); 93 }) 94 { 95 boost::contract::check c = boost::contract::constructor(this) __anon0c4c93340802null96 .postcondition([&] { 97 BOOST_CONTRACT_ASSERT(!moved()); 98 }) 99 ; 100 101 copy(other); 102 } 103 104 // Copy assignment. operator =(circular_buffer const & other)105 circular_buffer& operator=(circular_buffer const& other) { 106 // Moved-from can be (copy) assigned (so no pre `!moved()` here). 107 boost::contract::check c = boost::contract::public_function(this) 108 .precondition([&] { 109 BOOST_CONTRACT_ASSERT(!other.moved()); 110 }) 111 .postcondition([&] { 112 BOOST_CONTRACT_ASSERT(!moved()); 113 }) 114 ; 115 116 return copy(other); 117 } 118 read()119 char read() { 120 boost::contract::check c = boost::contract::public_function(this) 121 .precondition([&] { 122 BOOST_CONTRACT_ASSERT(!moved()); 123 }) 124 ; 125 126 unsigned i = index_++; 127 if(index_ == data_.size()) index_ = 0; // Circular. 128 return data_.at(i); 129 } 130 131 private: copy(circular_buffer const & other)132 circular_buffer& copy(circular_buffer const& other) { 133 data_ = other.data_; 134 index_ = other.index_; 135 moved_ = false; 136 return *this; 137 } 138 move(circular_buffer && other)139 circular_buffer& move(circular_buffer&& other) { 140 data_ = std::move(other.data_); 141 index_ = std::move(other.index_); 142 moved_ = false; 143 other.moved_ = true; // Mark moved-from object. 144 return *this; 145 } 146 147 std::vector<char> data_; 148 unsigned index_; 149 150 public: index() const151 unsigned index() const { 152 boost::contract::check c = boost::contract::public_function(this); 153 return index_; 154 } 155 size() const156 unsigned size() const { 157 boost::contract::check c = boost::contract::public_function(this); 158 return data_.size(); 159 } 160 }; 161 main()162 int main() { 163 struct err {}; 164 boost::contract::set_precondition_failure( 165 [] (boost::contract::from) { throw err(); }); 166 167 { 168 circular_buffer x({'a', 'b', 'c', 'd'}, 2); 169 assert(x.read() == 'c'); 170 171 circular_buffer y1 = x; // Copy constructor. 172 assert(y1.read() == 'd'); 173 assert(x.read() == 'd'); 174 175 circular_buffer y2({'h'}); 176 y2 = x; // Copy assignment. 177 assert(y2.read() == 'a'); 178 assert(x.read() == 'a'); 179 180 circular_buffer z1 = std::move(x); // Move constructor. 181 assert(z1.read() == 'b'); 182 // Calling `x.read()` would fail `!moved()` precondition. 183 184 x = y1; // Moved-from `x` can be copy assigned. 185 assert(x.read() == 'a'); 186 assert(y1.read() == 'a'); 187 188 circular_buffer z2({'k'}); 189 z2 = std::move(x); // Move assignment. 190 assert(z2.read() == 'b'); 191 // Calling `x.read()` would fail `!moved()` precondition. 192 193 x = std::move(y2); // Moved-from `x` can be move assigned. 194 assert(x.read() == 'b'); 195 // Calling `y2.read()` would fail `!moved()` precondition. 196 197 } // Moved-from `y2` can be destroyed. 198 199 return 0; 200 } 201 202