--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on October 2010 ---
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 |