ifdef.cpp 6.1 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213
  1. // Copyright (C) 2008-2018 Lorenzo Caminiti
  2. // Distributed under the Boost Software License, Version 1.0 (see accompanying
  3. // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
  4. // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
  5. #include <vector>
  6. #include <limits>
  7. #include <cassert>
  8. //[ifdef_function
  9. // Use #ifdef to completely disable contract code compilation.
  10. #include <boost/contract/core/config.hpp>
  11. #ifndef BOOST_CONTRACT_NO_ALL
  12. #include <boost/contract.hpp>
  13. #endif
  14. int inc(int& x) {
  15. int result;
  16. #ifndef BOOST_CONTRACT_NO_OLDS
  17. boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x);
  18. #endif
  19. #ifndef BOOST_CONTRACT_NO_FUNCTIONS
  20. boost::contract::check c = boost::contract::function()
  21. #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
  22. .precondition([&] {
  23. BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max());
  24. })
  25. #endif
  26. #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
  27. .postcondition([&] {
  28. BOOST_CONTRACT_ASSERT(x == *old_x + 1);
  29. BOOST_CONTRACT_ASSERT(result == *old_x);
  30. })
  31. #endif
  32. ;
  33. #endif
  34. return result = x++;
  35. }
  36. //]
  37. template<typename T>
  38. class pushable {
  39. #ifndef BOOST_CONTRACT_NO_ALL
  40. friend class boost::contract::access;
  41. #endif
  42. #ifndef BOOST_CONTRACT_NO_INVARIANTS
  43. void invariant() const {
  44. BOOST_CONTRACT_ASSERT(capacity() <= max_size());
  45. }
  46. #endif
  47. public:
  48. virtual void push_back(
  49. T const& x
  50. #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
  51. , boost::contract::virtual_* v = 0
  52. #endif
  53. ) = 0;
  54. protected:
  55. virtual unsigned capacity() const = 0;
  56. virtual unsigned max_size() const = 0;
  57. };
  58. template<typename T>
  59. void pushable<T>::push_back(
  60. T const& x
  61. #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
  62. , boost::contract::virtual_* v
  63. #endif
  64. ) {
  65. #ifndef BOOST_CONTRACT_NO_OLDS
  66. boost::contract::old_ptr<unsigned> old_capacity =
  67. BOOST_CONTRACT_OLDOF(v, capacity());
  68. #endif
  69. #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
  70. boost::contract::check c = boost::contract::public_function(v, this)
  71. #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
  72. .precondition([&] {
  73. BOOST_CONTRACT_ASSERT(capacity() < max_size());
  74. })
  75. #endif
  76. #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
  77. .postcondition([&] {
  78. BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
  79. })
  80. #endif
  81. ;
  82. #endif
  83. assert(false); // Shall never execute this body.
  84. }
  85. //[ifdef_class
  86. class integers
  87. #define BASES public pushable<int>
  88. :
  89. #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
  90. private boost::contract::constructor_precondition<integers>, BASES
  91. #else
  92. BASES
  93. #endif
  94. {
  95. #ifndef BOOST_CONTRACT_NO_ALL
  96. friend class boost::contract::access;
  97. #endif
  98. #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
  99. typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
  100. #endif
  101. #undef BASES
  102. #ifndef BOOST_CONTRACT_NO_INVARIANTS
  103. void invariant() const {
  104. BOOST_CONTRACT_ASSERT(size() <= capacity());
  105. }
  106. #endif
  107. public:
  108. integers(int from, int to) :
  109. #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
  110. boost::contract::constructor_precondition<integers>([&] {
  111. BOOST_CONTRACT_ASSERT(from <= to);
  112. }),
  113. #endif
  114. vect_(to - from + 1)
  115. {
  116. #ifndef BOOST_CONTRACT_NO_CONSTRUCTORS
  117. boost::contract::check c = boost::contract::constructor(this)
  118. #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
  119. .postcondition([&] {
  120. BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1));
  121. })
  122. #endif
  123. ;
  124. #endif
  125. for(int x = from; x <= to; ++x) vect_.at(x - from) = x;
  126. }
  127. virtual ~integers() {
  128. #ifndef BOOST_CONTRACT_NO_DESTRUCTORS
  129. // Check invariants.
  130. boost::contract::check c = boost::contract::destructor(this);
  131. #endif
  132. }
  133. virtual void push_back(
  134. int const& x
  135. #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
  136. , boost::contract::virtual_* v = 0
  137. #endif
  138. ) /* override */ {
  139. #ifndef BOOST_CONTRACT_NO_OLDS
  140. boost::contract::old_ptr<unsigned> old_size;
  141. #endif
  142. #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
  143. boost::contract::check c = boost::contract::public_function<
  144. override_push_back>(v, &integers::push_back, this, x)
  145. #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
  146. .precondition([&] {
  147. BOOST_CONTRACT_ASSERT(size() < max_size());
  148. })
  149. #endif
  150. #ifndef BOOST_CONTRACT_NO_OLDS
  151. .old([&] {
  152. old_size = BOOST_CONTRACT_OLDOF(v, size());
  153. })
  154. #endif
  155. #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
  156. .postcondition([&] {
  157. BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
  158. })
  159. #endif
  160. #ifndef BOOST_CONTRACT_NO_EXCEPTS
  161. .except([&] {
  162. BOOST_CONTRACT_ASSERT(size() == *old_size);
  163. })
  164. #endif
  165. ;
  166. #endif
  167. vect_.push_back(x);
  168. }
  169. private:
  170. #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
  171. BOOST_CONTRACT_OVERRIDE(push_back)
  172. #endif
  173. /* ... */
  174. //]
  175. public: // Could program contracts for these too...
  176. unsigned size() const { return vect_.size(); }
  177. unsigned max_size() const { return vect_.max_size(); }
  178. unsigned capacity() const { return vect_.capacity(); }
  179. private:
  180. std::vector<int> vect_;
  181. };
  182. int main() {
  183. integers i(1, 10);
  184. int x = 123;
  185. i.push_back(inc(x));
  186. assert(x == 124);
  187. assert(i.size() == 11);
  188. return 0;
  189. }