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] loop variant/assigns

  • Subject: [Frama-c-discuss] loop variant/assigns
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Wed, 7 Jan 2015 09:31:16 +0100
  • In-reply-to: <CAB73LL+ose8q20f-dF07NscU8YzOeScqu0MiABONys=ESHCFUw@mail.gmail.com>
  • References: <CAB73LL+ose8q20f-dF07NscU8YzOeScqu0MiABONys=ESHCFUw@mail.gmail.com>
Hi.

Using unsigned / signed is OK for WP in general.

Your invariants / variant properties rely on the monotony of division, which is not properly established by provers in general.
You should add a lemma like ? \forall x, 2 < p ==> x / p < x ? or an assertion after the instruction ? r /= k ; ?.

Other problems are about ? loop invariant 0 <= i < n ; loop assigns out[0..i] , i ; ? with ? for(i=0 ; i < n ; i++) ?.
The range invariant is wrong, the correct one is ? 0 <= i <= n ? (actually ? i==n ? at loop exit).
The loop assigns it is too precise for WP. You should use a larger loop assigns, say ? loop assigns out[0..n-1] , i ?.
Although, the loop assigns is not consistent with the function assigns contract, which states ?  assigns out[0] ? in your case.

Regards, L.

Le 6 janv. 2015 ? 19:17, DANIELA PEDRONI <daniela.pedroni at studenti.unipr.it> a ?crit :

> <base_conversion.c>