SPARK: gnatprove with -gnato13 option unrecognizable?

Question

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?

Answer 1

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)