Two source directories are delivered with each Kiasan invariant object.

Kiasan-Binary-Search-Tree-src Contains the original source used by the KSU group
                              which can be used with Kiasan/Sireum software 
                              anaylsis platform libraries located at
                                http://code.google.com/p/sireum/

Binary-Search-Tree-src        Contains source files that have no dependency on
                              Kiasan/Sireum libraries with annotations of the
                              contract specifications in JML (as comments).
                              No tools currently can process these JML
                              specifications directly.  You would need to use
                              these JML contract specs as guidance in forming
                              your own analysis tool-specific contract specs.

