search

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)
BSD 3-Clause "New" or "Revised" License
5 stars 3 forks source link

FunctionCallSubstitution uses legal Worthwhile identifiers for inserted return value variables #114

Closed bafain closed 12 years ago

bafain commented 12 years ago 
// 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.

jspam commented 12 years ago

f25d1ec07d847cb6f61448a8adbfa8aa115775c5 works towards fixing this.