blob: a8fd25d3f4cf044e2c9d08ec03e70bab56f6e800 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure{:layer 1}{:extern} P() returns(i:int);
procedure{:yields}{:layer 1,1}{:extern} Y({:layer 1}x:int);
procedure{:yields}{:layer 1,2} A({:layer 1}y:int)
ensures {:atomic} |{ A: return true; }|;
{
var{:layer 1} tmp:int;
call Y(y);
call tmp := P();
call Y(tmp);
}
|
