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=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.55.161.216 with SMTP id k207mr12520627qke.12.1509304635083;
        Sun, 29 Oct 2017 12:17:15 -0700 (PDT)
X-Received: by 10.157.91.109 with SMTP id e42mr613522otj.13.1509304635048;
 Sun, 29 Oct 2017 12:17:15 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.fcku.it!peer03.fr7!futter-mich.highwinds-media.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!z50no4982676qtj.0!news-out.google.com!r5ni5124qtc.1!nntp.google.com!z50no4982671qtj.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sun, 29 Oct 2017 12:17:14 -0700 (PDT)
In-Reply-To: <b6b12b92-cae8-4cf4-bda5-cdaf65383dec@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=149.32.224.37;
 posting-account=Qh2kiQoAAADpCLlhT_KTYoGO8dU3n4I6
NNTP-Posting-Host: 149.32.224.37
References: <81f4fbf9-fef3-4592-a95e-64889e564df4@googlegroups.com>
 <e995ba79-0762-43c0-a517-2b0dba562c46@googlegroups.com>
 <d10f711e-4dc8-45fa-8332-1e2af8965357@googlegroups.com>
 <cd703f4a-fb5c-4236-8ab2-b994db095981@googlegroups.com>
 <b6b12b92-cae8-4cf4-bda5-cdaf65383dec@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <81e99a7c-175a-42e8-82bb-83bebd5d4e68@googlegroups.com>
Subject: Re: What am I doing wrong with contracts?  Why are they succeeding
 when they should be failing?
From: Anh Vo <anhvofrcaus@gmail.com>
Injection-Date: Sun, 29 Oct 2017 19:17:15 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Body-CRC: 1623609403
X-Received-Bytes: 2571
Xref: news.eternal-september.org comp.lang.ada:48637
Date: 2017-10-29T12:17:14-07:00
List-Id: <comp.lang.ada>

On Sunday, October 29, 2017 at 6:42:09 AM UTC-7, Andrew Shvets wrote:
> On Sunday, October 29, 2017 at 3:20:15 AM UTC-4, joak...@kth.se wrote:
> > Den s=C3=B6ndag 29 oktober 2017 kl. 03:42:07 UTC+1 skrev Andrew Shvets:
> > > On Saturday, October 28, 2017 at 8:34:12 PM UTC-4, Andrew Shvets wrot=
e:
> > > > I think I'm misunderstanding how proofs/contracts work at some fund=
amental level.  Hence my confusion.
> > >=20
> > > I figured it out, I needed to have the following at the top of where =
the contract was written in order to have it be checked/enforced:
> > >=20
> > > pragma Assertion_Policy(Check);
> > >=20
> > > I'm reading more about this right now.
> >=20
> > To get run-time checks for the contracts you need to use the gcc Enable=
 Assertions flag "-gnata" during compilation.
> >=20
> > Best regards,
> > Joakim
>=20
> I just tried this.  It works.  Thanks for the tip.

I would prefer using pragma Assertion_Policy(Check) since it is 100% portab=
le.

Anh Vo