--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on January 2015 ---
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>