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] Why 2.27 released

  • Subject: [Frama-c-discuss] Why 2.27 released
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Fri, 15 Oct 2010 14:45:59 +0200
  • In-reply-to: <395817668.6335.1287058251768.JavaMail.root@zmbs1.inria.fr>
  • References: <4CB6C304.7@inria.fr> <395817668.6335.1287058251768.JavaMail.root@zmbs1.inria.fr>
On 10/14/2010 02:10 PM, Boris Hollas wrote:
> Two weeks ago, I posted the message "Binary search now works with
> Alt-Ergo 0.92". However, that same binary search function doesn't verify
> with why 2.27, as I've just tested. Both alt-ergo and CVC3 can't prove
> two crucial loop invariants. Was that function spuriously verified with
> why 2.26?
>    

Thanks again for reporting this problem with Why 2.27.
I confirm this is caused by the recent changes for the support of 
integer division.

For your particular example, I'd like to suggest to add in the code a 
statement
contract attached to the computation of mid as follows :

while(low <= high) {
     //@ ensures low <= mid <= high;   // this is the new annotation 
suggested
     mid = low + (high - low) / 2;
//    mid = (high + low) / 2;
     if (a[mid] < val) low = mid+1;
     else if(a[mid] > val) high = mid-1;
     else return mid;

It should improve the proofs a lot: for me, all provers Alt-Ergo, 
Simplify, Z3, CVC3 are able to solve the VCs quickly,
except 2 VCs for simplify, the 2 ones containing big ints that simplify 
does not support.

Generally speaking, adding such kinds of cuts can greatly help the 
provers. Unfortunately I have no recipe to find the good cuts, sorry. 
Here the idea is that a prover can be confused by division and try 
useless things, but the cut says
that it should not bother with this division: any other computation 
giving a number between low and high would
make the program correct.

There is no need to modify anything in Why 2.27. However, during my 
experiments I also tried to slightly
modify the file lib/why/divisions.why by adding a trigger. If you 
experience similar problems where division
is involved, you may also try the same: modify the axiom 
computer_div_mod as follows

axiom computer_div_mod:
   forall x,y:int [computer_div(x,y), computer_mod(x,y)].
     y <> 0 -> x = y * computer_div(x,y) + computer_mod(x,y)

Hope this helps,

- Claude

-- 
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                    |