СПАРК: gnatprove с опцией -gnato13 до неузнаваемости?

Question

Я очень новичок в Ada/SPARK. Я пытался следовать некоторым урокам отсюда -

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

Предположим, я запускаю приведенный здесь пример ISQRT ( http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html). Все коды (*.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 проверяющему, так что он пропустит некоторые проверки переполнения, но, по-видимому, этот параметр неприемлем.

любая идея?

Answer 1

"Помощь", оказанная 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

или во-вторых, установите это в георадаре (я использовал 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 знать, чтобы создать необходимые каталоги с -p флаг, но gnatprove делает это без ведома)