Skip to content

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

@mgrojo

Description

@mgrojo

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions