--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case



Hello,

Le jeu 19 mar 2009 09:40:47 CET,
David MENTRE <dmentre at linux-france.org> a ?crit :

> 
> I realized that more or less by trial and error. Is this written
> somewhere in Jessie documentation? I have probably read it but
> overlooked it.

There are a few words about loop invariants in section 2.1 of the
manual, but that could be more precise indeed.

> 
> By the way, I have seen that some "global" knowledge is also kept
> (assertions about global variables? function pre-condition?). Is this
> correct? Is this described somewhere?

I'm unsure what you mean by "global knowledge". assertion on variables
(and regions) that are not modified by the loop will still hold, but
that's all.

> I have a side question: I usually write \forall assertions with an
> int: "\forall int i; [...]". You write your assertion with "integer",
> "\forall integer i; [...]". Is there any difference? Any reason to
> prefer one over the other?

Technically, there are only integers in the logic, int is only a
shortcut to say 'I have an integer and it is between MIN_INT and
MAX_INT'. It exists mainly to be able to lift C lval in the logic, but
purely ACSL values should use the primitive type directly.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile