1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
-- basic test of right shift operator (Rumur extension)
var
x: -10 .. 10
y: 0 .. 4
z: boolean
startstate begin
z := true;
end
rule begin
x := 0;
-- right shift of 0 should still yield 0
x := x >> 0;
assert x = 0 ">> 0 yielded wrong value";
x := x >> 1;
assert x = 0 ">> 1 yielded wrong value";
y := 2;
x := x >> y;
assert x = 0 ">> 2 via variable yielded wrong value";
x := x >> -1;
assert x = 0 ">> -1 yielded wrong value";
x := x >> -4;
assert x = 0 ">> -4 yielded wrong value";
-- some general shift cases
x := 1 >> 1;
assert x = 0;
x := 2 >> 1;
assert x = 1;
x := 4 >> 2;
assert x = 1;
-- overshifts should always produce 0
x := 0 >> 128;
assert x = 0;
x := 1 >> 128;
assert x = 0;
x := 1 >> -128;
assert x = 0;
x := 2 >> 128;
assert x = 0;
x := y >> 128;
assert x = 0;
-- some negative shift cases
x := -1 >> 1;
assert x = -1;
x := -3 >> 1;
assert x = -2;
z := !z;
end
|
