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