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-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!s6g2000vbp.googlegroups.com!not-for-mail
From: Rod Chapman <roderick.chapman@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Clarification for SPARK postconditions on hidden subprograms.
Date: Fri, 26 Jun 2009 03:28:11 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <189c5cbe-10ce-46c7-89df-dcafcc78cfad@s6g2000vbp.googlegroups.com>
References: <898abcf6-7315-4015-9d73-d9365a870294@v2g2000vbb.googlegroups.com>
	<2bcddeb9-4823-469b-b496-d37f183fd929@s16g2000vbp.googlegroups.com>
	<b5695e1d-8385-4820-a710-94d269f0ddb3@r25g2000vbn.googlegroups.com>
NNTP-Posting-Host: 217.205.167.137
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1246012092 418 127.0.0.1 (26 Jun 2009 10:28:12
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 26 Jun 2009 10:28:12 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: s6g2000vbp.googlegroups.com; posting-host=217.205.167.137;
	posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.9.0.11)
	Gecko/2009060215 Firefox/3.0.11 GTB5 (.NET CLR 3.5.30729),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6636
Date: 2009-06-26T03:28:11-07:00
List-Id: <comp.lang.ada>

On Jun 26, 10:29=A0am, xorque <xorquew...@googlemail.com> wrote:
> =A0 82 =A0 =A0 =A0--# post ((Descriptor =A0=3D -1) -> (Error.Get_Error /=
=3D
> Error.Error_None)) or
> =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =
=A0 =A0 =A0 =A0^
> *** =A0 =A0 =A0 =A0Semantic Error =A0 =A0: =A03: Incorrect number of actu=
al
> parameters for call
> =A0 =A0 =A0 =A0 =A0 =A0of subprogram Get_Error.
> Does SPARK take issue with parameterless functions? Not unreasonable
> at all if this is the case, as SPARK should probably see them as
> constants.

Does this function have a global variable by any chance? If so, then
in annotations, you have to give additional actual parameters.
See section 3.3 of the Examiner_GenVCs manual.

> I hadn't made the connection until just now that you were the
> author of those. Thanks for writing those - there's a distinct lack
> of SPARK related info online.

We have very deliberately made the _entire_ set of manuals
available with the GPL release.  We hope in future to make
more tutorial-style information available on-line.

Yours,
 Rod Chapman, SPARK Team