You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: