--- 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



> 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