Console Output:
$ gnatprove -P main.gpr --checks-as-errors --level=0 --no-axiom-guard --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
read_record.adb:5:51: info: overflow check proved
read_record.adb:8:40: info: overflow check proved, in call inlined at read_record.adb:19
read_record.adb:8:40: info: index check proved, in call inlined at read_record.adb:19
read_record.adb:8:40: info: overflow check proved, in call inlined at read_record.adb:20
read_record.adb:8:40: info: index check proved, in call inlined at read_record.adb:20
Summary logged in /tmp/gnatprove/gnatprove.out
As the associated text says, the code is "correct and fully proved" but unless one takes a careful reading, it seems there are two errors still on lines 19 and 20, because they are highlighted in red, and when clicking the error icon is shown on those lines. It seems that all messages associated to a line and then with a second reference to another line are treated as errors.
For example, in this example: 03_Proof_Of_Program_Integrity example-8
As the associated text says, the code is "correct and fully proved" but unless one takes a careful reading, it seems there are two errors still on lines 19 and 20, because they are highlighted in red, and when clicking the error icon is shown on those lines. It seems that all messages associated to a line and then with a second reference to another line are treated as errors.