# Aste started: 2010-08-08 07:00:02 # Host id: Boogiebox # [2010-08-08 07:01:46] SpecSharp revision: 55320 # [2010-08-08 07:02:44] Boogie revision: 56211 # [2010-08-08 07:03:07] SscBoogie revision: 55325 [2010-08-08 07:03:31] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com SpecSharp.sln /Build DebugCommandLine warning CS1668 warning CS1668 [2010-08-08 07:04:57] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com Boogie.sln /Build Debug D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(4223,7): warning CS0162: Unreachable code detected D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(720,15): warning CS0162: Unreachable code detected D:\Temp\aste\Boogie\Source\VCGeneration\VCDoomed.cs(742,7): warning CS0162: Unreachable code detected D:\Temp\aste\Boogie\Source\VCGeneration\VCDoomed.cs(1084,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(856,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(339,7): warning CS0162: Unreachable code detected D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(364,7): warning CS0162: Unreachable code detected D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(380,7): warning CS0162: Unreachable code detected D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(403,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 D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(38,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(190,73): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(226,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(283,13): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(357,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(470,48): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(571,76): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(614,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(732,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'. 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 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 [2010-08-08 07:05:03] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com Dafny.sln /Build Debug D:\Temp\aste\Boogie\Source\Dafny\Parser.cs(760,18): warning CS0168: The variable 's' is declared but never used D:\Temp\aste\Boogie\Source\Dafny\Parser.cs(1340,72): warning CS0168: The variable 'id' is declared but never used D:\Temp\aste\Boogie\Source\Dafny\Parser.cs(1352,108): warning CS0168: The variable 'e' is declared but never used D:\Temp\aste\Boogie\Source\Dafny\Parser.cs(1890,15): warning CS0168: The variable 'tok' is declared but never used D:\Temp\aste\Boogie\Source\Dafny\Parser.cs(1890,31): warning CS0168: The variable 'e' is declared but never used D:\Temp\aste\Boogie\Source\Dafny\Parser.cs(1890,48): warning CS0168: The variable 'es' is declared but never used D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(39,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(187,73): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(220,21): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(302,13): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(371,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(426,23): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(457,44): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(572,76): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(617,48): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(735,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\AbsInt\bin\Debug\AbsInt.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'. warning CS0168 warning CS0168 warning CS0168 warning CS0168 warning CS0168 warning CS0168 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 warning CS0436 [2010-08-08 07:28:17] 1 out of 26 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed ['bitvectors'] # [2010-08-08 07:29:55] Released nightly of Boogie