From: joakimds@kth.se
Subject: Re: What am I doing wrong with contracts? Why are they succeeding when they should be failing?
Date: Sun, 29 Oct 2017 00:20:11 -0700 (PDT)
Date: 2017-10-29T00:20:11-07:00 [thread overview]
Message-ID: <cd703f4a-fb5c-4236-8ab2-b994db095981@googlegroups.com> (raw)
In-Reply-To: <d10f711e-4dc8-45fa-8332-1e2af8965357@googlegroups.com>
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
next prev parent reply other threads:[~2017-10-29 7:20 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 [this message]
2017-10-29 13:42 ` Andrew Shvets
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