Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
SymDiff

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.

Details

TypeDownload
File Namesymdiff.1.0.12.26.msi
Version1.1
Date Published26 December 2012
Download Size44.12 MB

Note By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license. Read the license.

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.

FAQ

Using Bit vectors for C

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".

Unnamed enumerated types

If your program contains constructs such as 

         enum {A, B} x;

then the resultant BPL file will not type check. The current (temporary) fix is to rewrite the source  as:

         enum <MyEnumName> {A, B} x;

 

 

Project Page
Related Links