New Features

Here’s what’s new in this release:

• First release of the SymDiff binaries
• Has a front-end for C programs (using the HAVOC front end)
• Has a front-end for Boogie programs
• Instructions to use bit-vectors with C programs

System Requirements

To run this software, you’ll need the following:

• A Windows Operating systems (such as Windows XP, Windows Vista, or Windows 7)
• A Visual Studio command prompt that can support "cl /analyze"

Installation Instructions

To install SymDiff, do the following:

1. Install the download into a directory with write permissions (e.g. "c:\symdiff1.0") that does not have a space (" ") in the directory path.
   1. Do not download it to the default ("c:\program files\Microsoft Research\") as suggested by the download link.
2. Follow the instructions listed in the SymDiff_manual.pdf present in the installation.

Using bit-vectors for C programs

If you wish to use bit-vectors for C programs, follow these additional steps (that will be automated in the future):

1. Add the flag "UseBvEncoding" to the list of TranslateFlags in the havoc_dlls\havoc.config file.
2. Search and change the following line the scripts\run_symdiff_c.cmd "... $notrace > $dir1name$dir2name.log" --> " ... $notrace /boogieOpt:/z3opt:RELEVANCY=0  > $dir1name$dir2name.log".

 

Project Page

• Symdiff project webpage

Contents

• New Features
• System Requirements
• Installation Instructions

Related Links

• HAVOC