DIFT.zip includes:

- 'conf_examples' file that has some of the examples of a conference manager system
- 'conf_examples_abrv' same as conf_examples but using global type and identifiers definitions
- 'simple_examples' file that illustrates some of our system and type system features 
- 'dropbox_examples' file that illustrates a toy dropbox service example 
- 'LambdaDIFT.jar' jar file that contains our typechecker prototype
- 'z3_linux', 'z3_mac' and 'z3_win' binaries of Z3 SMT Solver, version 4.3.2
- 'dift' (Unix) script file and 'dift.bat' (Windows) script file to give execution permissions to Z3 binaries and execute the jar containing the typechecker
-  Z3 dlls 'msvcp100.dll', 'msvcr100.dll', and 'vcomp100.dll'
- 'default_lattice' file containing the description of a security lattice
- 'short_manual.pdf' file containing a short manual of the typechecker
- this README

Synopsis:

sh dift [-help] [-input <filename>] [-output <filename>] [-debug <filename>] [-lattice <filename>] 


Executing the DIFT Typechecker prototype:

1 - Run 'sh dift' (Unix system) or 'dift.bat' (Windows) to execute the typechecker with the default options, that is using security lattice defined in 'default_lattice'.
2 - Execute command '#exit' to exit the typechecker

To execute (an) example(s) from a file:

1 - Run 'sh dift -input <filename>' (Unix system) or 'dift.bat -input <filename>' (Windows) to execute the typechecker with the default lattice, using the examples from file <filename>. 
For e.g., 'sh dift -input simples_examples' will execute the examples in file 'simple_examples'.

Programs always terminate with ';;', so a file can contain multiple programs separated by ';;'.
