blob: f5e082772cbb7182e6a0c64d3a53a9d48a1f733e (
plain)
1
2
3
4
5
6
7
8
9
10
|
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure A() {}
procedure B({:linear ""} tid:int) returns({:linear ""} tid':int)
{
tid' := tid;
call A();
}
|