blob: 633c24e81298378e1d1394e7926c6b5950351eb8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
// RUN: %boogie -proverWarnings:1 %s > %t
// RUN: %diff %s.expect %t
procedure foo2(x : bv32) returns(r : bv32)
{
block1:
r := x[-1:1]; // Error
// r := x[x:1]; // Error
r := x[1:x]; // Error
r := x[1+1:3]; // Error
return;
}
|