This project is read-only.

Today's VCC has a new Boogie (that hickups on my system)

Aug 6, 2010 at 2:58 PM
Edited Aug 9, 2010 at 8:54 AM

Hi all, Today's boogie hickups on my system (apologies for the formatting):

$ vcc /version 
Microsoft Research Vcc Version 2.1.30806.1 Microsoft Research Boogie Version 2.1.20806 Microsoft Research Z3 Version 2.0.40628.0 
Whereas yesterday: 
$ vcc /version Microsoft Research Vcc Version 2.1.30805.0 Microsoft Research Boogie Version 2.0.20616 Microsoft Research Z3 Version 2.0.40628.0
why i noticed this and what might be of general interest to me it looks that there is some update in the system requirements ... as for running today's VCC (2.1.30806.0) on (F# for Visual Studio 2008, 1.9.6.16; .NET Framework 4 Extended Beta 1; Visual C++ 2008 Express Edition with SP1) as I get 
$vcc test.c System.IO.FileNotFoundException: Could not load file or assembly 'Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16' or one of its dependencies. The system cannot find the file specified. File name: 'Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToke n=736440c9b414ea16' at Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstract Interpretation(Program program) at Microsoft.Research.Vcc.VccFunctionVerifier.PrepareBoogie(FSharpList`1 boogieDecls) in c:\ccnet\VccDrop\src\vcc\Host\VccPlugin.cs:line 280 at Microsoft.Research.Vcc.VccFunctionVerifier.Verify(String funcName) in c:\c cnet\VccDrop\src\vcc\Host\VccPlugin.cs:line 113 at Microsoft.Research.Vcc.VccCommandLineHost.VerifyFunctions(VccOptions comma ndLineOptions, String fileName, FunctionVerifier fver) in c:\ccnet\VccDrop\src\v cc\Host\Host.cs:line 413 at Microsoft.Research.Vcc.VccCommandLineHost.Felt2Cast2Plugin(String fileName , VccOptions commandLineOptions, HostEnvironment hostEnvironment, VccAssembly as sem) in c:\ccnet\VccDrop\src\vcc\Host\Host.cs:line 351 WRN: Assembly binding logging is turned OFF. To enable assembly bind failure logging, set the registry value [HKLM\Software\Microsoft\Fusion!EnableLog] (DWORD) to 1. Note: There is some performance penalty associated with assembly bind failure lo gging. To turn this feature off, remove the registry value [HKLM\Software\Microsoft\Fusion!EnableLog]. 
Everything is fine with 2.1.30805.0 still based on the old boogie to which I have reverted for now :-) 

Regards, Holger [Note: Christoph has independently reproduced this on one other system too.]

Aug 9, 2010 at 9:33 AM

Hi Holger,

thanks for pointing this out. As you noticed, there has been a proplem with a missing DLL after upgrading to a new Boogie version. This will be fixed in the next drop.

Stephan

Aug 10, 2010 at 11:30 AM
Hi Stephan, thanks for the fix. (Btw I'd be curious how you figured which DLL was missing from the above error message.) Running the regression with today's VCC seems fine (except for one target I only can check overnight), one thing that I noted (and already fixed in the verification target) is that "_();" (or "spec();") is now verboten in external declarations other than function definitions. (It's a bit inconsistent to allow then in external declaration other than function definitions things like e.g. ";_()" but that's sth I can live with...) Cheers,
Aug 10, 2010 at 11:36 AM

Hi Holger,

debugging that problem was simple - it was simply Microsoft.Contracts.dll, which was missing :-). Also, the problem could easily be reproduced on my machine as well.

Stephan

Sep 2, 2010 at 8:06 PM

Hi Stephan,

$ vcc /version

[...] Microsoft Research Boogie Version 2.1.20901.0

$ vcc /2 partition.h
System.TypeInitializationException: The type initializer for 'Microsoft.Boogie.CommandLineOptions' threw an exception. ---> System.IO.FileNotFoundException: Could not load file or assembly 'CodeContractsExtender, Version=2.1.20901.0, Culture=neutral, PublicKeyToken=736440c9b414ea16' or one of its dependencies. The system cannot find the file specified.
File name: 'CodeContractsExtender, Version=2.1.20901.0, Culture=neutral, PublicKeyToken=736440c9b414ea16'
   at Microsoft.Boogie.CommandLineOptions..cctor()

Now it's the extender of the fellow we had last time which looks like a rare birdie too :-) May I suggest inclusion into the installer?

On the positive side the syntax converter that in the meantime had been complaining about some missing dependency to F# seems to be working again :-)

Sep 3, 2010 at 6:28 AM

Thanks Holger - I have fixed the installer, removed the broken installer from the codeplex site and have triggered a new drop. The syntax converter problem had also occurred on Mark's machine while we were at VSTTE and I fixed it.

Sep 3, 2010 at 8:40 AM

Thanks Stephan - quick confirmation that the new drop runs smoothly here.