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 06:42:08 -0700 (PDT)
Date: 2017-10-29T06:42:08-07:00 [thread overview]
Message-ID: <b6b12b92-cae8-4cf4-bda5-cdaf65383dec@googlegroups.com> (raw)
In-Reply-To: <cd703f4a-fb5c-4236-8ab2-b994db095981@googlegroups.com>
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.
next prev parent reply other threads:[~2017-10-29 13:42 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 [this message]
2017-10-29 19:17 ` Anh Vo
2017-10-29 19:41 ` Andrew Shvets
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