blob: 45fdf7e4087ebf095e97d093e48c2283a54654e8 (
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;
}
|