From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.4 required=5.0 tests=AC_FROM_MANY_DOTS,BAYES_00, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Received: by 10.182.24.170 with SMTP id v10mr13591641obf.25.1431698648370; Fri, 15 May 2015 07:04:08 -0700 (PDT) X-Received: by 10.140.91.47 with SMTP id y44mr163210qgd.39.1431698648346; Fri, 15 May 2015 07:04:08 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!h15no3065794igd.0!news-out.google.com!k20ni14278qgd.0!nntp.google.com!z60no636763qgd.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 15 May 2015 07:04:08 -0700 (PDT) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=31.186.238.51; posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S NNTP-Posting-Host: 31.186.238.51 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: SPARK - precondition might fail (when there is no precondition) From: Maciej Sobczak Injection-Date: Fri, 15 May 2015 14:04:08 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:25885 Date: 2015-05-15T07:04:08-07:00 List-Id: Hi, Consider: -- p.ads: pragma SPARK_Mode; package P is =20 procedure Do_Nothing with No_Return; end P; -- p.adb: pragma SPARK_Mode; package body P is --pragma Warnings (Off); procedure Help_Doing_Nothing with No_Return; --pragma Warnings (On); =20 procedure Help_Doing_Nothing is begin loop null; end loop; end Help_Doing_Nothing; --Dummy : Integer; procedure Do_Nothing is begin --Dummy :=3D 0; Help_Doing_Nothing; end Do_Nothing; end P; There are two commented elements: a) pragma Warnings Off/On around declaration of a helper procedure b) Dummy integer variable with assignment that is there to look like an exe= cutable statement If a) is commented, then GNATProve (20140405) complains that Help_Doing_Not= hing has no effect. If a) is uncommented but b) is commented, the error message says that Do_No= thing has no effect and there is no complaint about Help_Doing_Nothing. If both a) and b) are uncommented, the error message says that precondition= might fail in the line where Do_Nothing calls Help_Doing_Nothing. All of these warnings can be seen with option --warnings=3Dcontinue. I sort of understand only the first message. The second case looks like SPA= RK is propagating the "has no effect" condition higher up the call chain. The third case is a complete mystery to me - what precondition might fail t= here? I understand that it is a precondition for Help_Doing_Nothing, but it= must be an implicit one and somehow the existence of variable D has an imp= act on it. I have failed to locate the precondition check in the files generated by GN= ATProve. Interestingly, the warning about precondition disappears when the aspect No= _Return is removed from Do_Nothing, so it must be a factor here as well - b= ut the SPARK RM does not describe any implicit preconditions related to sub= programs used from No_Return-ing callers. Any insight? If you have access to a newer version of the tool, is there any difference? --=20 Maciej Sobczak * http://www.inspirel.com