Am Samstag, dem 07.10.2023 um 14:38 +0300 schrieb Ville Voutilainen:
> On Sat, 7 Oct 2023 at 13:46, Martin Uecker via Liaison
> <liaison_at_[hidden]> wrote:
> >
> > Am Samstag, dem 07.10.2023 um 12:24 +0300 schrieb Timur Doumler:
> > You could make these additional arguments of the "macro":
> >
> > pre (x != 0, audit_level(3))
> >
> > or maybe:
> >
> > pre (<audit_level(3)>, x != 0)
>
> Indeed..
>
> pre(audit_level(3), x != 0)
>
> and something like
>
> > > void increment_size()
> > > post [old_size = size()] (size() == old_size + 1);
> >
> > You could do
> >
> > post ( [old_size = size()] (size() == old_size + 1) );
>
> post(capture(old_size = size()), size() == old_size + 1)
>
> 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?


>
> So.. at any rate, these suggestions are valuable, thanks for providing
> them. I think
> there is a way to fit them into the C++ syntax that we are designing,
> because we do similar
> things in other places. What the examples I wrote above illustrate are
> just instances
> of adding a prefix argument of a particular type to a pre/post "call"
> . It's essentially
> a tag argument. (And yes, we could equally well use postfix tags
> instead of prefix tags.)
>
> And the gist of what you're saying is that we should look into using
> such tags or any other
> techniques so that a a pre/post is always just "pre(whatever)" or
> "post(whatever)", and
> if we want to add bells and whistles, they should somehow go into the
> "whatever", not
> outside it, so no "[magic] pre(something)", no "pre<magic>(something)". Put that
> "magic" inside "something" and the syntax as a whole remains macroable
> and more C-friendly.

Yes, this would make it possible to hide this in macros and I would arge
that is also more friendly to C++ users who will have to do this.

Martin