After SPARK proofs pass, does the prover store this information and then the compiler use it to disable the runtime checks that are no longer needed? I couldn’t find this information anywhere.
1 Like
Nope, you need to disable it yourself, there is no GNAT <> gnatprove communication. Even if there was, you probably want to disable them anyways to support compilation without verification.
3 Likes
One way to potentially automate this is to create a shell script or Makefile which calls GNATprove && GNATmake without checks. If GNATprove errors out, GNATmake won’t be called without checks. You can expand this idea so that if GNATprove fails, then GNATmake is called with checks, debug info, etc 
Best regards,
Fer
How would the ObjectAda compiler know about the results from the prover?
There are also various pragmas such as suppress as some will want performance and some will want defense in depth or both in different places.