"Postconditions can access the function return value by declaring a variable
of type |auto| and assigning it to the |return| keyword (the variable name
is arbitrary but |result| is often used)."
What prevent the library to the use of return instead of an auto variable
postcondition( // Postconditions.
auto old_value = CONTRACT_OLDOF value, // Old value(s).
value == old_value + 1, // Assertion(s)...
return == old_value
)
This won't work if return is not the 1st token:
old_value == return
3 + return
myfync(return)
etc
because there's no way the preprocessor can skip the leading tokens
given that they are unknown :( and they could contain symbols. I will
clarify this point in the rationale.
instead of
postcondition( // Postconditions.
auto result = return, // Result value.
auto old_value = CONTRACT_OLDOF value, // Old value(s).
value == old_value + 1, // Assertion(s)...
result == old_value
)
As the old of value must be declared using a variable, using a specif oldof
keyword that will replace
auto old_size = CONTRACT_OLDOF size(),
by
oldofold_size = size(),
This wont' work because the pp can't separate the trailing size()
expression for the rest because it can't deal with unknown tokens and
symbols like "size()" or "old_size". The expression:
auto old_size = CONTRACT_OLDOF size()
is parsed into type "auto", assignment "old_size =" (note that the pp
can't separate the = because it's a symbol and that required lots of
tricks to be handled correctly...), and the expression "size()". I
need all these separate traits to handle old-values while:
oldofold_size = size()
and even:
oldof old_size = size()
can't separate "old_size = size()" into "old_size" and "size()". The
macro CONTRACT_OLDOF expands into )( so at some point in the
CONTRACT_FUNCTION expansion this:
CONTRACT_FUNCTION( ... auto old_size = CONTRACT_OLDOF size() ... )
expands to (auto is know or wrapped within parenthesis the user):
(auto) (old_size =) (size())
which is ultimately a sequence and it can be handled by the pp.
Log in to post a comment.
