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,48e1a3c594fb62e8
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,CP1252
Path: 
 g2news2.google.com!postnews.google.com!b7g2000yqk.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK
Date: Fri, 14 May 2010 01:11:29 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <06980a01-48c0-4405-9fa5-b05369997c1f@b7g2000yqk.googlegroups.com>
References: <op.vcl6900wule2fv@garhos> <op.vcodnferule2fv@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1273824689 3559 127.0.0.1 (14 May 2010 08:11:29
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 14 May 2010 08:11:29 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: b7g2000yqk.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:11598
Date: 2010-05-14T01:11:29-07:00
List-Id: <comp.lang.ada>

On 14 May, 04:07, Yannick Duch=EAne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> The Quick Reference Card #1 talks about =93type assertion=94:
>
> > A type assertion allows the user to specify the base type which the
> > compiler will associate with a signed integer type. The base type
> > must be supplied to the Examiner in the configuration file. This
> > assertion allows the Examiner to generate VCs which are much more
> > readily discharged [RTC 5.2].
>
> > Example:
> > type T is range 1 .. 10
> > --# assert T=92Base is Short_Short_Integer;
>
> As the Examiner ignore any representation clauses [SPARK 95 (13.1)], it =
=A0
> cannot care to any implicit representation clause either. So what's the =
=A0
> purpose of this kind of assertions ? Does the examiner check something =
=A0
> else which is not only the range ? Does it have something to deal with =
=A0
> type conversions ?
>
> --
> pragma Asset ? Is that true ? Waaww... great

Yannick,

These base type assertions are used to get the ranges for overflow
checks - see Section 5 of Generation of RTCs for SPARK Programs
(GenRTCs).

The Examiner can't validate this assertion, so it's up to the user to
get it right (but you might be able to use compiler assertions to
check it).  It is safe to assert a smaller base type than the compiler
actually chooses, so the portability problem can be reduced by
specifying the smallest possible base type.

Cheers,

Phil