adaspark-ada

SPARK: gnatprove with -gnato13 option unrecognizable?


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?


Solution

  • 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)