search

AdaCore / spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
GNU General Public License v3.0
249 stars 33 forks source link

Violation of GNATCheck rule 11.1.5.35 #26

Closed pjljvandelaar closed 3 years ago

pjljvandelaar commented 3 years ago

Dear AdaCore,

This project violates rule 11.1.5.35. Positional_Actuals_For_Defaulted_Generic_Parameters of Gnatcheck. See https://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gnatcheck_rm/predefined_rules.html#positional-actuals-for-defaulted-generic-parameters for more details about this rule.

Fortunately, this violation occurs only at one location in src/gnatprove/report_database.ads. A patch is automatically generated using the default settings of GNATPP. The patch is

@@ -48,8 +48,8 @@ package Report_Database is
       --  ??? Line and Column are Positive (or at least Natural)
    end record;

-   package Warning_Lists is new
-     Ada.Containers.Doubly_Linked_Lists (Suppressed_Warning, "=");
+   package Warning_Lists is new Ada.Containers.Doubly_Linked_Lists
+     (Suppressed_Warning, "=" => "=");

    --  Record of results obtained for a given subprogram or package
    type Stat_Rec is record

I will push this change as a pull request.

Greetings, Pierre

pjljvandelaar commented 3 years ago

Unfortunately you don't allow others to contribute

remote: Permission to AdaCore/spark2014.git denied to pjljvandelaar.
fatal: unable to access 'https://github.com/AdaCore/spark2014.git/': The requested URL returned error: 403

so I can't provide a pull request.

pjljvandelaar commented 3 years ago

When a argument is provided that is equal to the default value, it is useless and can be removed. The single violation I have found falls in this category!

GNATCheck has to my knowledge no check to report this fact. One could easily make a checker for this property and a rewriter to 'just' remove the provided argument.

kanigsson commented 3 years ago

Hello,

Sorry, this ticket seems to have slipped through the cracks. Concerning access rights, you should be able to fork the repository, and provide a pull request that way.

Concerning the actual content of this issue, we don't try to adhere to this Gnatcheck rule, and many other Gnatcheck rules, for example I'm pretty sure we violate the rule 11.1.5.36 which comes right after the rule you mention in the document you linked to. So I would be inclined to close the ticket without further action.