team-worthwhile/worthwhile — Issue #114: FunctionCallSubstitution uses legal Worthwhile identifiers for inserted return value variables
Author: bafain
Created: 2012-03-04 20:29:08+00:00
State: open

// EXPECTED:INVALID but ACTUAL:VALID
function Integer inc(Integer n)
_ensures _return = n + 1
{
return n + 1
}

Integer _inc0 := 0

while (_inc0 < 10)
_invariant _inc0 < 10
{
_inc0 := inc(_inc0)
}

_assert _inc0 = 10

The error is that `FunctionCallSubstitution` names the return value variable also `_inc0`.