On Sat, 7 Oct 2023 at 15:53, Martin Uecker <ma.uecker_at_[hidden]> wrote:
> > The capture one is interesting, and will be relevant for C, because it allows
> > writing a postcondition that uses the original value of a parameter even if your
> > function modifies the parameter. Such as if you get a pointer to a beginning and
> > return a pointer to something you were finding, you can just increment
> > the pointer
> > to the beginning, but you may want to check the original value in a
> > postcondition.
>
> Yes, although one could simply make the parameter const qualfied
> and do the copy the other way:
>
> int foo(const int size_in)
> _Postcondition (ret, ret <= size_in)
> {
> int size = size_in;
> ...
> return ret:
> }
>
> Then one could also do without this feature (and then it is not
> important whether C++ supports this or how). Or is there a
> use case I am missing?

That's certainly a possible work-around, but it also always incurs the
cost of the copy, even though
you really need the copy only when the contract is checked.