--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] loop variant/assigns



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>