Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Thu, 19 Mar 2009 09:40:47 +0100
  • In-reply-to: <20090318175434.1b258458@is005115>
  • References: <3d13dcfc0903180831t1002ccafhfa254b70595fac6a@mail.gmail.com> <20090318175434.1b258458@is005115>
Hello Virgile,

On Wed, Mar 18, 2009 at 17:54, Virgile Prevosto <virgile.prevosto at cea.fr> wrote:
> if the code of the reduced example is exactly like above, the assertion
> is not proved, since the lack of '@' means that it is not seen as an
> ACSL annotation.

Ohh! I'm ashamed. :-(

> If you put back the '@', there is another issue: the
> assertion is false. Namely, if you call f with n == 0, the loop is not
> entered, and total is still 0 at this point.

Ah yes. I realized that in my larger example that's why I wrote the
following pre-condition.

> Now the larger example has a stronger pre-condition (0<
> num_candidates). So why does alt-ergo still fail on the assertion?
> Well, remember that the only thing that jessie 'knows' after a loop is
> its invariant,

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.

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?

> and here the loop invariant is too weak: it gives an
> upper bound for total, but no lower bound. A possibility (short of the
> ACSL construction \sum which is currently unsupported by jessie) would
> be to add the following invariant:
>
> loop invariant \forall integer j; 0<=j<i ==> total >= counters[j];

Thank you. I'll try that.

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?

Sincerely yours,
david