From: Andrew Shvets <andrew.shvets@gmail.com>
Subject: Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
Date: Sun, 29 Oct 2017 12:41:45 -0700 (PDT)
Date: 2017-10-29T12:41:45-07:00 [thread overview]
Message-ID: <6a777f1d-ece9-4c50-a451-25aa7defd549@googlegroups.com> (raw)
In-Reply-To: <81e99a7c-175a-42e8-82bb-83bebd5d4e68@googlegroups.com>
On Sunday, October 29, 2017 at 3:17:15 PM UTC-4, Anh Vo wrote:
> 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öndag 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 wrote:
> > > > > I think I'm misunderstanding how proofs/contracts work at some fundamental level. Hence my confusion.
> > > >
> > > > 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:
> > > >
> > > > pragma Assertion_Policy(Check);
> > > >
> > > > I'm reading more about this right now.
> > >
> > > To get run-time checks for the contracts you need to use the gcc Enable Assertions flag "-gnata" during compilation.
> > >
> > > Best regards,
> > > Joakim
> >
> > I just tried this. It works. Thanks for the tip.
>
> I would prefer using pragma Assertion_Policy(Check) since it is 100% portable.
>
> Anh Vo
I agree. That I'd forget the compiler flag from time to time and think my code was working when it wasn't.
next prev parent reply other threads:[~2017-10-29 19:41 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-10-29 0:31 What am I doing wrong with contracts? Why are they succeeding when they should be failing? Andrew Shvets
2017-10-29 0:34 ` Andrew Shvets
2017-10-29 2:42 ` Andrew Shvets
2017-10-29 7:20 ` joakimds
2017-10-29 13:42 ` Andrew Shvets
2017-10-29 19:17 ` Anh Vo
2017-10-29 19:41 ` Andrew Shvets [this message]
2017-10-30 0:16 ` Shark8
2017-10-30 1:37 ` Andrew Shvets
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox