1

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?

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。

(少なくとも) 2 つの方法があります。まず、-cargsルートを使用します。

gnatprove -P t1q4.gpr -cargs -gnato13

または2番目に、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 に答える