Sketch#: Sketching in Spec#

This tool is a fork from: 
    Boogie v54898 (http://boogie.codeplex.com/)
    SpecSharp v54900 (http://specsharp.codeplex.com/)


BUILD INSTRUCTIONS
------------------

A. Builld SscSharp [* Run as Admin ]

   cd $SKETCH#\SpecSharp\SpecSharp\Microsoft.SpecSharp\LastKnownGood9
   clean.cmd
   RegisterLKG.cmd

   cd $SKETCH#\SpecSharp\SpecSharp
   devenv SpecSharp.sln /build DebugCommandLine
   devenv SpecSharp.sln /build Debug

B. Build Boogie/SscBoogie

   cd $SKETCH#\Boogie\Binaries
   nmake
   cd ..\Source
   devenv Boogie.sln /build Debug
   cd ..\..\SpecSharp\SscBoogie\Binaries
   nmake
   cd ..\Source
   devenv SscBoogie.sln /build Debug
   cd ..\Binaries
   nmake register

COMPILING INSTRUCTIONS
----------------------

$SKETCH#\Boogie\Binaries\ssc.exe /debug+ <FILENAME>.ssc

    * Notes: 
      
        /debug+ is required!

SKETCHING INSTRUCTIONS
----------------------

$SKETCH#\SpecSharp\SscBoogie\Binaries\SscBoogie.exe /sketch <Options> <FILENAME>.exe

    * Notes: 
      
        /sketch is required!

    * Attributes on method declarations:
        
        [Inline]	    : inlines body (same holes on each instance)
        [Inline][Generator] : inlines body (fresh holes on each instance)

    * Options:

        /proverLog:C:\Temp\z3-@PROC@

            store Z3 call logs for various sketching steps for debugging
        
        /traceSketch

            print sketching related debug info
    
        /numCEGARItrs:N        

            MAX number of CEGAR based synthesis iterations (default = 10)

        /numRandInpGen:N       

            number of random tuples for CEGAR synthesis (default = 1)

	/intBits:N
	
	    bit width for integer holes (allowed = {8, 16, 32}, default = 8)
	
        /numThreads:N

            runs Parallel Z3 with N threads (default = 0)

	/unboundRandInpArrLen

            do not impose implicit array length bound (= 10) when generating random arrays as input

CONTACT
------------------
Please send mail to Hesam Samimi (hesam@ucla.edu) if there are any problems