--- layout: fc_discuss_archives title: Message 128 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] unproven VC with newer why version



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