1

我对 Ada/SPARK 很陌生。我试图从这里学习一些教程——

http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html

假设我正在运行此处给出的 ISQRT 示例 ( http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#id19 )。所有代码（*.ads和*.adb）都捆绑为一个名为的项目isqrt.gpr，我正在运行的命令是——

:~$ gnatprove -gnato13 -P isqrt.gpr

我得到的输出是——

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.

该教程说我需要提供一个调用证明者的开关-gnato13，以便它跳过一些溢出检查。但显然这个开关是不可接受的。

任何想法？

4

1 回答 1

3

该gnatprove命令给出的“帮助”非常有用：

$ 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
...

并且没有提到的gnatprove开关是-gnato13.

因此，您需要将开关传递给在后台gnatprove使用的编译器。

有两种方式（至少）：首先，使用-cargs路线，

gnatprove -P t1q4.gpr -cargs -gnato13

或者第二，在 GPR 中设置它（我用过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;

（for Object_Dir use ".build”;将中间文件隐藏在通常不可见的子目录中；gprbuild并且知道使用标志gnatmake创建所需的目录，但没有被告知）-pgnatprove

于 2014-11-13T13:58:12.967 回答