Found by Paul Eibensteiner, the following program should verify, but Viper complains about an undeclared identifier 'var_m2', even though that variable is visible at the call site.
define m1(res) {
res := var_m2
}
define m2(res) {
var var_m2: Int
var v0_1: Int
{
m1(v0_1)
}
res := var_m2
}
method caller() returns (value: Int)
{
var res: Int
{
m2(res)
}
var value2: Int
{
m2(res)
}
value := res
}
Found by Paul Eibensteiner, the following program should verify, but Viper complains about an
undeclared identifier 'var_m2'
, even though that variable is visible at the call site.