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] unproven VC with newer why version

Jens Gerlach wrote:
>
> Am 08.12.2009 um 14:54 schrieb Claude Marche:
>
>
>>>
>> add "loop variant n-i;" and you should be done !
>
> I had a look at section "loop variants" (page 37) 
> in http://frama-c.cea.fr/download/acsl-implementation-Beryllium-20090902.pdf 
> .
> It says
>
> Optionally, a loop annotation may include a loop variant of the form
> ...
> where m is a term of type integer .
> The semantics is as follows: for each loop iteration that terminates 
> normally or with continue, the value of m at end of the iteration must 
> be smaller 
> that its value at the beginning of the iteration. Moreover, its value 
> at the beginning must be nonnegative. Note that the value of m at loop 
> exit might be negative. 
> It does not compromise termination of the loop. 
>
> It would be nice if this section would be more explicit that in 
> general loop variants are necessary for (automatic?) provers because ...
>
This document documents the ACSL language, and is not tight to any tool 
to verify the annotations. Your concern is only
related to the way Jessie/Why handles termination. Until Why 2.21,
when the user did not give any loop variant the termination was simply 
not checked. Some user claimed that it could make one think, if all VC 
are proved, that its program is correct whereas it is not.

Hence we decided that we should be as defensive as possible, and since 
Why 2.22 termination is always required to be proved.

Since the demand seems important, I announce that in the next release of 
Jessie/Why, it is possible to ask for forgetting about termination
via a new pragma

# pragma JessieTerminationPolicy(never)

which ask to forget about termination completely and

# pragma JessieTerminationPolicy(user)

which generates VC for termination only where loop variants or decreases 
clauses were given. (Which was the behavior of Why 2.21)

If there is a strong demand for that, we can produce a new Jessie/Why 
release quickly.

- Claude

> Regards
>
> Jens
> ------------------------------------------------------------------------
>
> _______________________________________________
> 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                    |