Two source directories are delivered with each Kiasan invariant object.

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

Binary-Heap-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.

