--- layout: fc_discuss_archives title: Message 128 from Frama-C-discuss on December 2009 ---
Hello, so is it correct, that at the moment there is no way to specify and prove a non-terminating function, that I want to be non-terminating ? As terminates \false; is ignored by Jessie one VC (variant decreases) remains unproven. Can I conclude it just means that I have a function that doesnt terminate (which I know about and is not problematic) but the rest is ok or does it affect maybe other VC's, that maybe are proven unwanted then. Regards, Kerstin -----Urspr?ngliche Nachricht----- Von: frama-c-discuss-bounces at lists.gforge.inria.fr im Auftrag von Claude Marche Gesendet: Di 08.12.2009 14:54 An: Frama-C public discussion Betreff: Re: [Frama-c-discuss] unproven VC with newer why version Jens Gerlach wrote: > We were able to deductively verify the following implementation of > linear search successfully with Jessie on top of why version 2.19. > > However, with why 2.23 there is one safety related VC that remains > unproven. > In the jessie gui, the unproven VC reads "variant decreases". > > Do we have to improve the specification to get rid of that issue? > If so, how? add "loop variant n-i;" and you should be done ! Since Why 2.22, the policy for generating termination VCS is as strict as possible, to guarantee soundness (see BTS #0000103) In the future, Jessie should support ACSL "terminates" clauses, to manually annotate function for which you don;t care about termination. In a nearer future, there could a new pragma to control the generation of such VCs. Anyway: any suggestion welcome ! - Claude > > Regards Jens > > /*@ > requires n >= 0; > requires \valid_range(a, 0, n-1); > > assigns \nothing; > > behavior some: > assumes \exists int i; (0 <= i < n) && a[i] == v; > ensures 0 <= \result < n; > ensures a[\result] == v; > ensures \forall int i; (0 <= i < \result) ==> a[i] != v; > > behavior none: > assumes \forall int i; (0 <= i < n) ==> a[i] != v; > ensures \result == n; > */ > int find(const int* a, int n, int v) > { > /*@ > loop invariant 0 <= i <= n; > loop invariant \forall int k; 0 <= k < i ==> a[k] != v; > */ > for (int i = 0; i < n; ++i) > if (a[i] == v) > return i; > > return n; > } > > > -- > > Dr.-Ing. Jens Gerlach > Eingebettete Systeme - EST > Tel.: +49 (0)30 6392 1841 > Fax.: +49 (0)30 6392 1805 > E-Mail: jens.gerlach at first.fraunhofer.de > <mailto:jens.gerlach at first.fraunhofer.de> > > Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST > Kekul?stra?e 7 > 12489 Berlin > Germany > http://www.first.fraunhofer.de > > > > > ------------------------------------------------------------------------ > > _______________________________________________ > 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 -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex | _______________________________________________ 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 -------------- A non-text attachment was scrubbed... Name: not available Type: application/ms-tnef Size: 4605 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091217/68650837/attachment.bin