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

# [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
• 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                    |

```