--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why 2.27 released



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                    |