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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,4e0df1f3e9a1ac5d
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!k22g2000yqh.googlegroups.com!not-for-mail
From: George <geo.paok@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK: Problem with using constants in a post annotation
Date: Thu, 13 Jan 2011 01:26:01 -0800 (PST)
Organization: http://groups.google.com
Message-ID: 
 <dc91014e-abf4-4553-86f1-9bf929b45503@k22g2000yqh.googlegroups.com>
References: <af7b3e83-d76b-4a65-831f-4251a1b2a51c@z5g2000yqb.googlegroups.com>
NNTP-Posting-Host: 155.207.113.40
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
X-Trace: posting.google.com 1294910762 19143 127.0.0.1 (13 Jan 2011 09:26:02
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 13 Jan 2011 09:26:02 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: k22g2000yqh.googlegroups.com; posting-host=155.207.113.40;
 posting-account=6UhNNwoAAAAqPvbGV2FILHuA9mXqxy3m
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
 Trident/4.0; GTB6.6; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
 3.0.30729; Media Center PC 6.0; InfoPath.2; .NET4.0C),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:16412
Date: 2011-01-13T01:26:01-08:00
List-Id: <comp.lang.ada>


PLEASE IGNORE THE PREVIOUS. THE FOLLOWING IS A CORRECT VERSION OF THE
MESSAGE:

Hello,

I'm trying to use inside a post annotation two constants that are
declared in the package body. But, I can't do it, because the two
constants are not recognised at the point where they are used in the
annotation. Does anyone have an idea of how to overcome this problem?
Is it possible to overcome this by using only annotations without
changing the code?
The package specification and body, as well as the error messages are
shown below:

-- File P2.ads
--# inherit P1;
package P2
is
   procedure Proc;
   --# global in out P1.Val;
   --# derives P1.Val from P1.Val;
   --# post (P1.Val <= C1 -> P1.Val = 0) and  -- error appears here
   --#      (P1.Val >= C2 -> P1.Val = 1);     -- error appears here

end P2;


-- File P2.adb
with P1;
package body P2 is

   C1: constant P1.Type := 10;
   C2: constant P1.Type := 20;

   procedure Proc
   is
      V1: P1.Type;
   begin
      V1 := P1.Val;
      if V1 <= C1 then
         P1.Val := 0;
      elsif V1 >= C2 then
         P1.Val := 1;
      end if;
   end Proc;

end P2;


OUTPUT
13:30   Semantic Error   1 - The identifier C1 is either undeclared or
not visible at this point.
14:30   Semantic Error   1 - The identifier C2 is either undeclared or
not visible at this point.