Am Samstag, dem 07.10.2023 um 16:10 +0300 schrieb Ville Voutilainen:
> 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.

In C this should not matter, because the compiler should be able
to remove the copy in all cases. (Although in practice compilers are
bad at this for arguments.). I guess in C++ it might not always
be possible.

Martin