---
layout: fc_discuss_archives
title: Message 46 from Frama-C-discuss on December 2009
---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Lemma from ACSL doc doesn't verify
- Subject: [Frama-c-discuss] Lemma from ACSL doc doesn't verify
- From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
- Date: Thu, 3 Dec 2009 13:03:30 +0100
- In-reply-to: <4B17A5C1.2040409@inria.fr>
- References: <FC0686BB6178BC43B9DC035287A11A720DBE657C91@SI-MBX12.de.bosch.com> <20091125162200.0a3ccb44@is010235> <FC0686BB6178BC43B9DC035287A11A720DBE657D6B@SI-MBX12.de.bosch.com> <4B17A5C1.2040409@inria.fr>
> But the way, for using these lemmas in your codes, PLEASE USE TYPE
> integer INSTEAD OF TYPE int
> /@ lemma mean_property: \forall integer l, h; l <= h ==> l <= l + (h-l)/2 <= h;
> - Claude
If I use
/@ lemma mean_property2: \forall integer l, h; l <= h ==> l <= (l+h)/2 <= h;
Instead of the lemma above and try to use it for numbers of type int, will the prover detect that mean_property2 doesn't hold for int as (l+h) may overflow?
-Boris