Output contract's arguements

[Maxim Fomin]

On Wednesday, 18 September 2013 at 12:11:03 UTC, monarch_dodra 
wrote:
> This came up in learn:
> Say you have this code:
>
> //----
> size_t msb(T)(T v)
> in
> {
>   assert(v != 0);
> }
> out(ret)
> {
>   assert(v != 0); //Fails? Passes?
> }
> body
> {
>   size_t ret = 0;
>   while(v >>= 1) ++ret;
>   return ret;
> }
> //----
>
> Question, can this output contract fail?

It may or may not fail depending on language definition and right 
now spec lacks clarification.

>
> Apparently, it does fail, since it is passed the variable v, 
> *after* the body of the function is done with it.
>

It currently fails due to the way in-body-out are implemented: 
all block statements are united into essentially one function. 
Body block (or some other entity) doesn't 'pass' variable, it is 
out block which refers to local modified value is an issue (cmpl  
  $0x0,-0x8(%rbp)). You could find it yourself by looking into 
assembly.

> IMO, this is wrong. When calling a function with an out 
> contract, the arguments should *also* be passed to the out 
> contract directly. "out" should not be expected to run on the 
> body's "sloppy seconds".
>

Probably if you think that parameters should be 'passed'. I don't 
think that implementation should behave this way. I also find no 
reason why out contract should refer to unmodified argument.

> In particular if/when we will have "contracts are 
> managed/compiled by caller", then that behavior is the only 
> behavior we will be able to do (AFAIK).
>

I looks like your misunderstanding based on wrong assumption 
about implementation.

> Or is there something that explicitly states it works that way? 
> Should I file a bug report? ER?

I don't consider that whether out refers to unmodified or 
modified parameter is important issue. Current policy should be 
just documented and left as it is (unless you provide significant 
reasons that current implementation is flawed).