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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,45974c4ba2f5422c,start X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!b9g2000yqm.googlegroups.com!not-for-mail From: xorque Newsgroups: comp.lang.ada Subject: Hide annotations on procedures. Date: Fri, 12 Jun 2009 06:35:10 -0700 (PDT) Organization: http://groups.google.com Message-ID: NNTP-Posting-Host: 81.86.41.187 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1244813711 7130 127.0.0.1 (12 Jun 2009 13:35:11 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 12 Jun 2009 13:35:11 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: b9g2000yqm.googlegroups.com; posting-host=81.86.41.187; posting-account=D9GNUgoAAAAmg7CCIh9FhKHNAJmHypsp User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.0.7) Gecko/2009030814 Iceweasel/3.0.9 (Debian-3.0.9-1),gzip(gfe),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:6445 Date: 2009-06-12T06:35:10-07:00 List-Id: Having failed to take the day off from learning SPARK, I've run into a strange problem regarding procedure annotations. I have the following in a package body: procedure C_Readlink_Boundary (File_Name : in String; Buffer : out String; Buffer_Size : in File.File_Name_Index_t; Returned_Size : out C_Types.Signed_Size_t) is --# hide C_Readlink_Boundary begin null; end C_Readlink_Boundary; The body of the procedure is obviously not implemented yet. The procedure itself is defined only in the body of the package, not accessible from outside. The body of the procedure is intended to be hidden from SPARK. The problem I have is that SPARK doesn't seem to get it: 7 procedure C_Readlink_Boundary ^ *** Semantic Error :154: The subprogram or task body C_Readlink_Boundary does not have an annotation. The procedure doesn't touch any global variables. Any 'derives' annotation added to the procedure is rejected by SPARK (as it would need to go on the procedure specification - which doesn't exist). I've used the same pattern on functions, not procedures, and SPARK has accepted it. What have I done wrong here?