Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Info messages are highlighted as errors when they have a reference to a second line and column numbers #1049

Open
mgrojo opened this issue May 12, 2024 · 0 comments

Comments

@mgrojo
Copy link

mgrojo commented May 12, 2024

For example, in this example:
03_Proof_Of_Program_Integrity example-8

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant