How to install and build the sources
Install and Build for Visual Studio 2010
After downloading the sources via the "Source Code" tab, check to make sure you have any
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. If you get errors
saying that RegAsm could not load a dll, try unblocking that dll (right-click the file ==> Properties ==> Unblock).
- 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
- 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
- Note that to run the Spec# verifier with a new version, you need to build SscBoogie, as described below.
SscBoogie (after successfully building Spec#)
- Navigate to the SscBoogie\Binaries directory, and edit the definition of variable
BOOGIEROOT in Makefile to point to your Boogie installation. If you didn't build into the Registration directory in the steps for building Spec# above, then you will also need to change
the variable REG_DIR to point to your
LastKnownGood10 directory. Then, type nmake at a command prompt (this makes local copies of various needed Spec# binaries).
- In the SscBoogie\Source directory, either open
SscBoogie10.sln in Visual Studio and build the Debug configuration, or from a command prompt type
devenv SscBoogie10.sln /build Debug.
- In the SscBoogie\Test directory, execute
runtestall.bat. 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).
Install and Build for Visual Studio 2008 (not officially supported anymore)
If you have the option, we strongly recommend using Visual Studio 2010, since this is the version Spec# is currently developed and tested with. However, if you need to compile with 2008, you can follow the same instructions above, after making the following
change. For each of the following three files, find the two occurrences of ";DEV10" (which should be within "DefineConstants" tags), and delete them (just the DEV10 - leave the other constants there):