SymDiff, a language-agnostic tool for equivalence checking and displaying semantic (behavioral) differences over imperative programs. The tool operates at the level of the intermediate verification language Boogie, and hence language-agnostic. This download contains a front end for comparing C programs compiled using the Microsoft C compiler.
Note By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license. Read the license.
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
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"
To install SymDiff, do the following:
- Install the download into a directory with write permissions (e.g. "c:\symdiff1.0") that does not have a space (" ") in the directory path.
- Do not download it to the default ("c:\program files\Microsoft Research\") as suggested by the download link.
- 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):
- Add the flag "UseBvEncoding" to the list of TranslateFlags in the havoc_dlls\havoc.config file.
- Search and change the following line the scripts\run_symdiff_c.cmd "... $notrace > $dir1name$dir2name.log" --> " ... $notrace /boogieOpt:/z3opt:RELEVANCY=0 > $dir1name$dir2name.log".