Diagnosys Prototype


The prototype implementation of Diagnosys is available in this tarball. It includes various components that are described in this section.

  • SHAna : the semantic match files specifying the analysis of for all categories of safety holes with their respective launch scripts. It includes SmPL, Ocaml and bash code.

  • DIGen : the generator of interface wrappers. It includes Ocaml and bash code.

  • Dlog : the userspace utility for activating/deactivating Diagnosys and for retrieving log traces