How to install and build the sources for Visual Studio 2010 (for 2008, see remarks below)
After downloading the sources via the "Source Code" tab, check to make sure you have any External Dependencies
that you need. Then use the following directions for the program(s) you want to build. Some of them have extra dependencies. Note:
- Some users have reported problems when working under cygwin due to unexpected access permissions and file ownership; we strongly recommend using the Visual Studio 2010 Command Prompt.
- Navigate to the SpecSharp\Microsoft.SpecSharp\LastKnownGood10 directory. Execute "Clean.cmd" and "RegisterLKG.cmd". You will need to have Administrator privileges in order to execute these scripts, and you need regasm.exe on your path (you may need to right-click on the Visual Studio 2010 Command Prompt and select Run as Administrator). This registers the Spec# compiler that comes in the LastKnownGood10 directory with Visual Studio so that Spec# projects can be loaded into Visual Studio and built. Some of the projects in the compiler are Spec# projects: the compiler is partially boot-strapped.
- Open up SpecSharp10.sln in Visual Studio 2010 and build the "Debug" configuration (which should be selected by default). Right click on the "Checkin Tests" project and build it to make sure the regressions pass (one of the regression tests fails if the language of your Windows installation is not English; just ignore that test case).
- The previous step builds a new version of the Spec# binaries. If you want to register the new version with Visual Studio, then you should close the Visual Studio IDE, and (using a command prompt with administrator privileges) navigate to the SpecSharp\Microsoft.SpecSharp\Registration directory. Execute "RegisterCurrent.cmd" to register your new version with Visual Studio. If you want to deregister this version, execute the "Clean.cmd" script in this directory.
- If your registered version of Spec# becomes unusable in VisualStudio for any reason, you can try deregistering and registering it again, by repeating (with Visual Studio closed) either step 1 (to go back to the bootstrap version) or step 3 (for your currently-compiled version) above.
- Note that to run the Spec# verifier with a new version, you need to build SscBoogie, as described below.
SscBoogie (after successfully compiling Spec#)
- Navigate to the SscBoogie\Binaries directory, and type nmake at a command prompt (this makes local copies of various needed Spec# binaries).
- In the SscBoogie\Source directory, either open SscBoogie.sln in Visual Studio and build the Debug configuration, or from a command prompt type devenv SscBoogie.sln /build Debug.
- In the SscBoogie\Test directory, execute runtestall.bat short. Let us know if something doesn't succeed!
- Go back to the SscBoogie\Binaries directory and type nmake register at the command prompt (this copies the binaries for the verifier back to where Spec# can find them).