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

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>