From 483eb2f56657e8e7f419ab1a4fab8dce9ade8609 Mon Sep 17 00:00:00 2001 From: Daniel Baumann Date: Sat, 27 Apr 2024 20:24:20 +0200 Subject: Adding upstream version 14.2.21. Signed-off-by: Daniel Baumann --- .../libs/contract/example/features/access.cpp | 95 ++++++++++++++++++++++ 1 file changed, 95 insertions(+) create mode 100644 src/boost/libs/contract/example/features/access.cpp (limited to 'src/boost/libs/contract/example/features/access.cpp') diff --git a/src/boost/libs/contract/example/features/access.cpp b/src/boost/libs/contract/example/features/access.cpp new file mode 100644 index 00000000..07586172 --- /dev/null +++ b/src/boost/libs/contract/example/features/access.cpp @@ -0,0 +1,95 @@ + +// 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 + +#include +#include +#include + +template +class pushable { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(capacity() <= max_size()); + } + +public: + virtual void push_back(T const& value, boost::contract::virtual_* v = 0) + = 0; + +protected: + virtual unsigned capacity() const = 0; + virtual unsigned max_size() const = 0; +}; + +template +void pushable::push_back(T const& value, boost::contract::virtual_* v) { + boost::contract::old_ptr old_capacity = + BOOST_CONTRACT_OLDOF(v, capacity()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(capacity() < max_size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + }) + ; + assert(false); +} + +//[access +template +class vector + #define BASES public pushable + : BASES +{ // Private section of the class. + friend class boost::contract::access; // Friend `access` class so... + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // ...private bases. + #undef BASES + + void invariant() const { // ...private invariants. + BOOST_CONTRACT_ASSERT(size() <= capacity()); + } + + BOOST_CONTRACT_OVERRIDE(push_back) // ...private overrides. + +public: // Public section of the class. + void push_back(T const& value, boost::contract::virtual_* v = 0) + /* override */ { + boost::contract::old_ptr old_size = + BOOST_CONTRACT_OLDOF(v, size()); + boost::contract::check c = boost::contract::public_function< + override_push_back>(v, &vector::push_back, this, value) + .precondition([&] { + BOOST_CONTRACT_ASSERT(size() < max_size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + }) + ; + + vect_.push_back(value); + } + + /* ... */ +//] + + unsigned size() const { return vect_.size(); } + unsigned max_size() const { return vect_.max_size(); } + unsigned capacity() const { return vect_.capacity(); } + +private: // Another private section. + std::vector vect_; +}; + +int main() { + vector vect; + vect.push_back(123); + assert(vect.size() == 1); + return 0; +} + -- cgit v1.2.3