--- layout: fc_discuss_archives title: Message 3 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



Many thanks Lo?c,
I've expanded the range of output_buffer in the external assigns and I
added the assertion in the loop. However both the assigns and the loop
variant are still incorrect (method's code in the attachment).
In the manual ACSL 1.8 (Neon implementation)
<http://frama-c.com/download/acsl-implementation-Neon-20140301.pdf>at page
38 is state that: "Optionally, a loop annotation may include a lo op
variant of the form /*@ loop variant m; */ where m is a term of type
integer" , so if there's no integer which decrease within the loop, can I
omit the loop variant ?

Best regards,
Daniela Pedroni
<http://frama-c.com/download/acsl-implementation-Neon-20140301.pdf>

2015-01-07 9:31 GMT+01:00 Lo?c Correnson <loic.correnson at cea.fr>:

> 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>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150111/9ef0f20c/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: calculate_output.c
Type: text/x-csrc
Size: 1239 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150111/9ef0f20c/attachment.c>