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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
# Aste started: 2010-08-24 07:00:04
# Host id: Boogiebox
# [2010-08-24 07:02:12] SpecSharp revision: 55320
# [2010-08-24 07:03:15] Boogie revision: 56714
# [2010-08-24 07:03:39] SscBoogie revision: 56316
[2010-08-24 07:04:15] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com SpecSharp.sln /Build DebugCommandLine
warning CS1668
warning CS1668
[2010-08-24 07:05:13] [Error] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com Boogie.sln /Build Debug
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(825,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2804,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\Absy.cs(3472,9): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\Core\Parser.cs(783,91): warning CS0168: The variable 'id2' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(866,98): warning CS0168: The variable 'locals' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(866,120): warning CS0168: The variable 'blocks' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(1123,47): warning CS0168: The variable 'e' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(1377,112): warning CS0168: The variable 'op' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(1684,17): warning CS0168: The variable 'ty' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(1807,36): warning CS0168: The variable 'e' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(1807,53): warning CS0168: The variable 'es' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(1808,27): warning CS0168: The variable 'key' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(1808,40): warning CS0168: The variable 'value' is declared but never used
D:\Temp\aste\Boogie\Source\Core\Parser.cs(1915,23): warning CS0168: The variable 'value' is declared but never used
D:\Temp\aste\Boogie\Source\Core\OOLongUtil.cs(109,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\Core\Util.cs(21,10): warning CS0414: The field 'Microsoft.Boogie.TokenTextWriter.writerOpenedHere' is assigned but its value is never used
D:\Temp\aste\Boogie\Source\Core\VCExp.cs(139,16): warning CS0414: The field 'Microsoft.Boogie.ProverOptions.sequenceNumber' is assigned but its value is never used
D:\Temp\aste\Boogie\Source\VCExpr\VCExprAST.cs(1467,16): warning CS0659: 'Microsoft.Boogie.VCExprAST.VCExprCustomOp' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\VCExpr\VCExprAST.cs(662,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCExpr\VCExprASTPrinter.cs(46,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1933,56): warning CS0168: The variable 'e' is declared but never used
D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(4602,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(707,15): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\VCDoomed.cs(741,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\VCDoomed.cs(1083,11): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\Wlp.cs(77,8): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\Check.cs(379,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\Check.cs(445,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(843,29): warning CS0649: Field 'VC.VCGen.Split.first_assert' is never assigned to, and will always have its default value null
D:\Temp\aste\Boogie\Source\VCGeneration\DoomCheck.cs(177,22): warning CS0169: The field 'VC.DoomCheck._tmpUseFreshBVars' is never used
D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(65,9): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(338,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(363,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(379,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(402,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(111,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(290,7): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(308,7): warning CS0162: Unreachable code detected
C:\Windows\Microsoft.NET\Framework\v3.5\Microsoft.Common.targets : warning MSB3245: Could not resolve this reference. Could not locate the assembly "Microsoft.Z3". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors.
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(11,17): error CS0234: The type or namespace name 'Z3' does not exist in the namespace 'Microsoft' (are you missing an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ContextLayer.cs(11,17): error CS0234: The type or namespace name 'Z3' does not exist in the namespace 'Microsoft' (are you missing an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\StubContext.cs(11,17): error CS0234: The type or namespace name 'Z3' does not exist in the namespace 'Microsoft' (are you missing an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\TypeAdapter.cs(11,17): error CS0234: The type or namespace name 'Z3' does not exist in the namespace 'Microsoft' (are you missing an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ProverLayer.cs(11,17): error CS0234: The type or namespace name 'Z3' does not exist in the namespace 'Microsoft' (are you missing an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(18,17): error CS0246: The type or namespace name 'Term' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(19,31): error CS0246: The type or namespace name 'Term' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(23,16): error CS0246: The type or namespace name 'Term' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(31,17): error CS0246: The type or namespace name 'Pattern' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(32,34): error CS0246: The type or namespace name 'Pattern' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(36,16): error CS0246: The type or namespace name 'Pattern' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(44,17): error CS0246: The type or namespace name 'FuncDecl' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(45,36): error CS0246: The type or namespace name 'FuncDecl' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(49,16): error CS0246: The type or namespace name 'FuncDecl' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(57,17): error CS0246: The type or namespace name 'Sort' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(58,27): error CS0246: The type or namespace name 'Sort' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(62,16): error CS0246: The type or namespace name 'Sort' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(71,17): error CS0246: The type or namespace name 'LabeledLiterals' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(72,38): error CS0246: The type or namespace name 'LabeledLiterals' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(76,16): error CS0246: The type or namespace name 'LabeledLiterals' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(84,45): error CS0246: The type or namespace name 'Symbol' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(93,16): error CS0246: The type or namespace name 'Context' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(161,22): error CS0246: The type or namespace name 'Term' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(172,22): error CS0246: The type or namespace name 'Pattern' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(183,17): error CS0246: The type or namespace name 'Sort' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(189,17): error CS0246: The type or namespace name 'Term' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(195,17): error CS0246: The type or namespace name 'FuncDecl' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(201,37): error CS0246: The type or namespace name 'Term' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(206,42): error CS0246: The type or namespace name 'FuncDecl' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(211,40): error CS0246: The type or namespace name 'Pattern' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(224,22): error CS0246: The type or namespace name 'Sort' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(312,57): error CS0246: The type or namespace name 'Model' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(443,22): error CS0246: The type or namespace name 'Symbol' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(451,17): error CS0246: The type or namespace name 'Symbol' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(550,17): error CS0246: The type or namespace name 'FuncDecl' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(562,19): error CS0246: The type or namespace name 'Context' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(564,34): error CS0246: The type or namespace name 'Context' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\SafeContext.cs(569,33): error CS0246: The type or namespace name 'Sort' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ContextLayer.cs(22,17): error CS0246: The type or namespace name 'Config' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ContextLayer.cs(57,16): error CS0246: The type or namespace name 'Config' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ContextLayer.cs(204,66): error CS0246: The type or namespace name 'Model' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ContextLayer.cs(236,67): error CS0246: The type or namespace name 'Model' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ContextLayer.cs(247,79): error CS0246: The type or namespace name 'Model' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ContextLayer.cs(318,64): error CS0246: The type or namespace name 'Model' could not be found (are you missing a using directive or an assembly reference?)
D:\Temp\aste\Boogie\Source\Provers\Z3api\ContextLayer.cs(324,46): error CS0246: The type or namespace name 'Model' could not be found (are you missing a using directive or an assembly reference?)
error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Z3api\bin\Debug\Provers.Z3api.dll' could not be found
warning CS0659
warning CS0659
warning CS0162
warning CS0168
warning CS0168
warning CS0168
warning CS0168
warning CS0168
warning CS0168
warning CS0168
warning CS0168
warning CS0168
warning CS0168
warning CS0168
warning CS0162
warning CS0414
warning CS0414
warning CS0659
warning CS0162
warning CS0162
warning CS0168
warning CS0162
warning CS0162
warning CS0162
warning CS0162
warning CS0162
warning CS0162
warning CS0162
warning CS0649
warning CS0169
warning CS0162
warning CS0162
warning CS0162
warning CS0162
warning CS0162
warning CS0162
warning CS0162
warning CS0162
45 error
1 error
2 failed
|
