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
|
using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Text;
using Microsoft.Boogie;
/// <summary>
/// A class containing static methods to extend the functionality of Code Contracts
/// </summary>
public static class cce {
[Pure]
public static T NonNull<T>(T t) {
Contract.Assert(t != null);
return t;
}
[Pure]
public static bool NonNullElements<T>(IEnumerable<T> collection) {
return collection != null && Contract.ForAll(collection, c => c != null);
}
[Pure]
public static bool NonNullElements(VariableSeq collection) {
return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
}
public class UnreachableException : Exception {
public UnreachableException() {
}
}
[Pure]
public static void BeginExpose(object o) {
}
[Pure]
public static void EndExpose() {
}
public static bool IsPeerConsistent(this object o) {
return true;
}
public static bool IsConsistent(this object o) {
return true;
}
public static bool IsExposable(this object o) {
return true;
}
public static class Owner {
[Pure]
public static bool Same(object o, object p) {
return true;
}
}
}
public class PeerAttribute : System.Attribute {
}
public class RepAttribute : System.Attribute {
}
public class CapturedAttribute : System.Attribute {
}
|
