blob: 38d696b7b1f2ecfe4342e4d315a936de9df6ac52 (
plain)
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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace RegressionTestInput {
[AttributeUsage(AttributeTargets.Method)]
public class AsyncAttribute : Attribute { }
public class Class0 {
static int StaticInt;
static int StaticMethod(int x) {
return x + 1;
}
void M(int x) {
int y = (5 / x) + (x = 3);
Contract.Assert(x == 3 && y <= 8);
StaticInt = y;
Contract.Assert(y == StaticInt);
}
// Test to make sure we generate unique procedure names
void M(int x, int y) { }
void M(bool b) { }
void M(Class0 c) { }
int NonVoid() {
return 3 + StaticInt + StaticMethod(3);
}
int OutParam(out int x) {
x = 3 + StaticInt;
return x;
}
int RefParam(ref int x) {
x = x + 1;
StaticInt = x;
return x;
}
int AssignToInParam(int x) {
x = x + 1;
StaticInt = x;
return x;
}
[AsyncAttribute]
int MethodThatRepresentsAnAynchronousMethod(int x) {
return x;
}
int CallAsyncMethod(int y) {
return MethodThatRepresentsAnAynchronousMethod(y);
}
}
class ClassWithBoolTypes {
static bool staticB;
bool b;
static bool M(int x, int y) {
return x < y;
}
public ClassWithBoolTypes(bool z) {
this.b = z;
if (z) ClassWithBoolTypes.staticB = z;
}
public static void Main() {
ClassWithBoolTypes.M(3, 4);
}
}
class ClassWithArrayTypes
{
public static void Main1()
{
int[] s = new int[5];
s[0] = 2;
Contract.Assert(s[0] == 2);
int[] t = new int[4];
t[0] = 1;
Contract.Assert(t[0] == 1);
Contract.Assert(s[0] == 2);
}
public static int[] s;
public static void Main2()
{
s = new int[5];
s[0] = 2;
Contract.Assert(s[0] == 2);
int[] t = new int[4];
t[0] = 1;
Contract.Assert(t[0] == 1);
Contract.Assert(s[0] == 2);
}
public int[] a;
public void Main3(int x)
{
a[x] = 42;
a[x + 1] = 43;
Contract.Assert(a[x + 1] == a[x] + 1);
}
}
}
|
