Project Hi-Lite / GNATprove

spacer

Part of the Hi-Lite project, GNATprove is a formal verification tool for Ada, based on the GNAT compiler. It can prove that subprograms respect their contracts, expressed as preconditions and postconditions in the syntax of Ada 2012. The tool automatically discovers the subset of subprograms which can be formally analyzed. GNATprove is currently available for x86 linux, x86 windows and x86-64 linux.

DOWNLOAD GNATprove

You should first install GNAT GPL 2012, and then GNATprove at the same location. Under Linux, put the path "your location"/bin in your PATH variable. Under Windows, the installation takes care of this step.

To use the integration of GNATprove in GPS, download the GNATprove plug-in and copy it either in the share/gps/plug-ins/ subdirectory of your GPS installation, or in $HOME/.gps/plug-ins (where $HOME is your home directory).

ACCESS ONLINE DOC

(also available in pdf format)


See GNATprove in action inside GNAT Programming Studio


Known problems:
  • On Windows, GNATprove only works when applied to projects under the C: drive.

For questions, remarks, problems, please contact us on

hi-lite-discuss@lists.forge.open-do.org

Learn More about Project Hi-Lite

  • Categories

  • Open-DO Projects

    Agile
    Couverture
    GeneAuto/Ada
    HiberSource
    Hi-Lite
    Project P
    The Qualifying Machine
    XReq
  • Want to get involved?

    The Open-DO Forge
  • Contact

    info @ open-do.org
  • Blogroll

    • carlodaffara.conecta.it
    • David A. Wheeler's Blog
    • David Crocker's Verification Blog
    • Emmanuel Chenu
    • Frama-C news and ideas
    • Herding Cats
    • Rustan Leino's Verification Corner
    • The Abnormal Distribution
  • Meta

    • Log in
gipoco.com is neither affiliated with the authors of this page nor responsible for its contents. This is a safe-cache copy of the original web site.