I am very new to Ada/SPARK. I was trying to follow some tutorials from here --
http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html
Suppose I am running the ISQRT example given here (http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#id19). All the codes (*.ads and *.adb) are bundled as a project called isqrt.gpr and the command that I am running is --
:~$ gnatprove -gnato13 -P isqrt.gpr
and the output I am getting is --
Phase 1 of 3: frame condition computation ...
Phase 2 of 3: analysis and translation to intermediate language ...
Phase 3 of 3: generation and proof of VCs ...
analyzing isqrtsubtyped, 0 checks
analyzing isqrtsubtyped.ISQRT, 13 checks
isqrtsubtyped.ads:7:31: warning: overflow check might fail
gprbuild: *** compilation phase failed
gnatprove: error during generation and proof of VCs, aborting.
The tutorial says I need to supply a switch called -gnato13 to the prover so that it will skip some of the overflow checks., but apparently this switch is not acceptable.
any idea?
The ‘help’ given by the gnatprove command is quite useful:
$ gnatprove --help
Usage: gnatprove -Pproj [files] [switches] [-cargs switches]
proj is a GNAT project file
files is one or more file names
-cargs switches are passed to gcc
...
and none of the mentioned gnatprove switches is -gnato13.
So what’s happening is that you need to get the switch passed to the compiler that gnatprove is using under the hood.
There are two ways (at least): first, use the -cargs route,
gnatprove -P t1q4.gpr -cargs -gnato13
or second, set this up in the GPR (I used t1q4.gpr),
project T1Q4 is
for Source_Files use ("t1q4.ads", "t1q4.adb");
for Object_Dir use ".build";
package Compiler is
for Default_Switches ("ada") use ("-gnato13");
end Compiler;
end T1Q4;
(the for Object_Dir use ".build”; hides intermediate files away in a usually-invisible subdirectory; gprbuild and gnatmake know to create required directories with the -p flag, but gnatprove does it without being told)