SPARK: 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#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, чтобы он пропустил некоторые проверки переполнения., Но, по-видимому, этот переключатель неприемлем.

любая идея?

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 делает это без bei ng said)