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



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                    |