Skip to content

procedure to run GNATprove not complete #3

Description

@yannickmoy

I think you should add that, prior to do proof, one should copy Why3 theory files in the SPARK installation under share/spark/theories:

cp formal-numerics/theories/* /path/to/spark/install/share/spark/theories

Currently, this is a bit hidden under gnatprove branch in the README.md, together with all instructions to build gnatprove, which are not needed anymore with SPARK GPL 2014.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions