2021-03-05 01:04 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001251Frama-CPlug-in > jessiepublic2013-03-27 09:44
Assigned Tocmarche 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001251: Binary search doesn't verify anymore after upgrade
DescriptionAfter upgarding to why 2.31 and why3 0.73, my binary search program doesn't verify with Alt-Ergo, Z3, and CVC3 and a timeout of 10s.

In particular, the
loop invariant \forall integer i; 0 <= i < low ==> a[i] < val;
doesn't verify.

The code did verify with the previous version of Jessie and it verifies with wp.

The same is true for another program, mismatch.c.

This is a show stopper as the binary search is frequently used to demonstrate formal verification.
TagsNo tags attached.
Attached Files
  • c file icon mismatch.c (699 bytes) 2012-07-31 10:53 -
    /*@	requires \valid(a+(0..length-1)) && \valid(b+(0..length-1));
        ensures  (\forall integer k; 0 <= k < length ==> a[k] == b[k])  ==>  \result == -1;
        ensures !(\forall integer k; 0 <= k < length ==> a[k] == b[k])  ==>  0 <= \result < length && a[\result] != b[\result];
    	assigns \nothing;
    int mismatch(int a[], int b[], int length)
    	int k;
    	/*@	loop invariant \forall integer l; 0 <= l < k ==> a[l] == b[l];
    		loop invariant 0 <= k;
    		loop assigns k;
    		loop variant length - k;
    	for (k = 0; k < length; k++)
    		if(a[k] != b[k]) return k;
    	return -1;
    int main() {
    	int a[] = {12,4,5,3,99};
    	int b[] = {12,4,6,2,99};
    	int k;
    	k = mismatch(a, b, 5);
    	//@assert k == 2;
    	return 0;
    c file icon mismatch.c (699 bytes) 2012-07-31 10:53 +
  • c file icon binary-search.c (1,190 bytes) 2012-08-20 20:27 -
    /*@ predicate Sorted{L}(int *a, integer l, integer r) =
    		\forall integer i,j; l <= i < j <= r ==> a[i] <= a[j];
    /*@ requires \valid(a+ (0..a_length-1)) && a_length >= 0;
    	requires Sorted(a,0,a_length-1);
    	assigns \nothing;
    	behavior success:
    		assumes \exists integer res; 0 <= res <= a_length-1 && a[res] == val;
    		ensures 0 <= \result <= a_length-1	&&	a[\result] == val;
    	behavior failure:
    		assumes !(\exists integer res; 0 <= res <= a_length-1 && a[res] == val);
    		ensures \result == -1;
    	complete behaviors;
    	disjoint behaviors;
    int bsearch(int a[], int a_length, int val) {
    	int low, mid, high;
    	low = 0; high = a_length-1;
    	/*@ loop invariant 0 <= low && high <= a_length-1;
    		loop invariant \forall integer i; 0 <= i < low  ==>  a[i] < val;
    		loop invariant \forall integer i; high < i <= a_length-1  ==>  a[i] > val;
    		loop assigns low, high, mid;
    		loop variant high-low;
    	while(low <= high) {
    		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;
    	return -1;
    int main() {
    	int a[6] = {1,3,4,6,8,19};
    	int k = bsearch(a, 6, -8);
    	//assert k == -1;
    	return 0;
    c file icon binary-search.c (1,190 bytes) 2012-08-20 20:27 +
  • html file icon bts1251.html (10,998 bytes) 2012-08-21 13:30
  • png file icon gWhy.png (281,751 bytes) 2012-08-21 15:05
  • ? file icon .why3.conf (1,358 bytes) 2012-08-21 18:18
  • ? file icon .whyrc (458 bytes) 2012-08-21 18:19
  • ? file icon why3.conf (327 bytes) 2012-08-22 13:27
  • html file icon binary-search.html (3,117 bytes) 2012-08-22 20:36




cmarche (developer)

The attached file is mismatch.c and does not contain a binary search function.
Please provide the proper example so that I can figure out the problem.


boris (reporter)

Sorry, this is the binary search file.


cmarche (developer)

I can't reproduce the problem, for me the program is proved.

I attach the results I obtained with several versions of those provers, see bts1251.html.

Please give more info on what is not proved on your side.


cmarche (developer)

By the way, you could send your own results by sending the .xml file that is located in


note that the html file can be generated using

  why3session html binary-search.jessie/binary-search

resulting in a file



boris (reporter)

As bts1251 shows, Alt-Ergo and CVC3 time-out why trying to prove

loop invariant \forall integer i; 0 <= i < low ==> a[i] < val;

The same happens on my system with Z3 4.0. It used to verify with Alt-Ergo with the previous version of why. However, it verifies with Simplify. I use the command line

frama-c -jessie -jessie-atp=gui -pp-annot

since the why3 gui doesn't work (see why3 bug 14672).

Unfortunately, there is no .xml-file located in any subdirectory:

~/progs/c/frama-c/binary-search$ find . -type f -name *.xml

Therefore, I can't generate an html-file:
~/progs/c/frama-c/binary-search$ why3session html binary-search.jessie/binary-search

anomaly: Not_found


cmarche (developer)

Sorry, I did not understand you were using Why2 GUI, not Why3.

Could you send me your ~/.why3.conf so that I can try to figure out what is the problem with Why3 ?

Alos, did you do "why3config --detect" ?


boris (reporter)

I haven't done "why3config --detect" yet. This command gives an error

The plugin /usr/local/lib/why3/plugins/tptpfof.cmxs dynlink failed :
Dynlink error : error loading shared library: /usr/local/lib/why3/plugins/tptpfo

but it detects my provers. If I now run

frama-c -jessie binary-search.c

I still get

[jessie] Calling VCs generator.
why3ml [...] binary-search.mlw

field 'name' is missing
make: *** [why3ml] Error 1
[jessie] user error: Jessie subprocess failed: make -f binary-search.makefile why3ml

I reported this as bug 14672 in the why3 bts.


cmarche (developer)

I am still trying to understand the problem but no success yet. Please could you attach the following file ?



cmarche (developer)

Sorry, I don't understand where is the problem.

I tried to make fresh install of why3 0.73 and why 2.31 and the problem does not show up with me.

The only possibility I see would be that for some reason your why3 does not use the ~/.why3.conf generated but some other configuration file. Could you check that?

One possible try: run manually the command

why3ide --debug-all t.jessie/t.mlw

and send me what is printed on screen


boris (reporter)

Maybe you mean binary-search instead of t?

~/progs/c/frama-c/binary-search$ why3ide --debug-all binary-search.jessie/binary-search.mlw
<0.011314>[Info] Init the GTK interface...<0.017468> done.
<0.017506>[Info] reading icons...<0.037217> done.
<0.074332>[Info] Creating tree model...<0.075364> done
<0.103482>[Info] found regular file 'binary-search.jessie/binary-search.mlw'
<0.103531>[Info] using 'binary-search.jessie/binary-search' as directory for the project
<0.103573>[Info] 'binary-search.jessie/binary-search' does not exists. Creating directory of that name for the project
<0.103685>[Info] Opening session...
            <0.103715>[Info] update_session: shape_version = 2
            <0.103741>[Info] update_session: done
            <0.103754>[Sched] init scheduler max=2
[Info] Opening session: done
<0.103845>[Info] adding file ../binary-search.mlw in database
<0.103868>[Load] file '../binary-search.mlw'
Error while reading file '../binary-search.mlw':
Library file not found: jessie3

/usr/local/lib$ find . -type f -name jessie3*

/usr/local/lib$ ocamlc -v
The Objective Caml compiler, version 3.12.1
Standard library directory: /usr/lib/ocaml

I use Debian 7.


cmarche (developer)

Last edited: 2012-08-22 16:58

I'm surprised that the error "field name is missing" does not show up.
What happens if you do

  why3ide --debug-all --extra-config /usr/local/lib/why/why3/why3.conf binary-search.jessie/binary-search.mlw

and then if you retry

  frama-c -jessie binary-search.c



boris (reporter)

~/progs/c/frama-c/binary-search$ why3ide --debug-all --extra-config /usr/local/lib/why/why3/why3.conf binary-search.jessie/binary-search.mlw

field 'name' is missing
~/progs/c/frama-c/binary-search$ frama-c -jessie binary-search.c
[kernel] preprocessing with "gcc -C -E -I. -dD binary-search.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir binary-search.jessie
[jessie] File binary-search.jessie/binary-search.jc written.
[jessie] File binary-search.jessie/binary-search.cloc written.
[jessie] Calling Jessie tool in subdir binary-search.jessie
Generating Why function bsearch
Generating Why function main
[jessie] Calling VCs generator.
why3ml [...] binary-search.mlw

field 'name' is missing
make: *** [why3ml] Error 1
[jessie] user error: Jessie subprocess failed: make -f binary-search.makefile why3ml


cmarche (developer)

Then this shows that the problem is related to /usr/local/lib/why/why3/why3.conf

But still I don't see why...

could you edit the file /usr/local/lib/why/why3/why3.conf and remove the section headed by [prover coq], and try again please ?

Indeed you can remove everything except the first two lines
loadpath = " ..."


cmarche (developer)

Even better: I've now been able to reproduce the bug !

The [prover coq] section appearing in /usr/local/lib/why/why3/why3.conf causes problem if
Coq is not installed, which is your case.

OK, thanks for your time, I'm now able to fix the problem.

In the meantime, removing the [prover coq] section should work for you


boris (reporter)

Alright, I can use why3 now. While the binary search itself now verifies, the call in main doesn't. I split all unproven goals until no further split was possible. Yet, "Function main, Safety" runs in a time-out (see attachment).


cmarche (developer)

The problem with main unproved is related to the weaknesses of Jessie regarding allocation. I guess you mean it was proved with Why2 before ?


boris (reporter)

Yes, all VCs in binary-search.c were proved with the previous version of Why2/Jessie and Alt-Ergo.


cmarche (developer)

Indeed you found another bug ! it was introduced by the migration of the Jessie memory model from Why2 to Why3.

You can fixed yourselves, by modifying the file


look for this
val free_parameter (a:ref (alloc_table 't)) (p:pointer 't) :
  { p = null (* allowed, see man 3 free *) /\
and change the last /\ by \/

This is fixed in the devt version. I think we are going to make a bug-fix release of Why 2 soon,

Thanks again for testing and finding thoses bugs !


signoles (manager)

Fixed in Frama-C Oxygen + Why 2.32.

-Issue History
Date Modified Username Field Change
2012-07-31 10:53 boris New Issue
2012-07-31 10:53 boris Status new => assigned
2012-07-31 10:53 boris Assigned To => cmarche
2012-07-31 10:53 boris File Added: mismatch.c
2012-08-20 14:06 cmarche Note Added: 0003401
2012-08-20 20:27 boris File Added: binary-search.c
2012-08-20 20:28 boris Note Added: 0003403
2012-08-21 13:30 cmarche File Added: bts1251.html
2012-08-21 13:31 cmarche Note Added: 0003404
2012-08-21 13:35 cmarche Note Added: 0003405
2012-08-21 15:05 boris Note Added: 0003407
2012-08-21 15:05 boris File Added: gWhy.png
2012-08-21 15:58 cmarche Note Added: 0003408
2012-08-21 18:18 boris Note Added: 0003409
2012-08-21 18:18 boris File Added: .why3.conf
2012-08-21 18:19 boris File Added: .whyrc
2012-08-22 12:41 cmarche Note Added: 0003411
2012-08-22 13:27 boris File Added: why3.conf
2012-08-22 13:47 cmarche Note Added: 0003412
2012-08-22 14:35 boris Note Added: 0003413
2012-08-22 16:31 cmarche Note Added: 0003414
2012-08-22 16:58 cmarche Note Edited: 0003414
2012-08-22 17:09 boris Note Added: 0003415
2012-08-22 17:38 cmarche Note Added: 0003416
2012-08-22 17:44 cmarche Note Added: 0003417
2012-08-22 20:36 boris File Added: binary-search.html
2012-08-22 20:39 boris Note Added: 0003418
2012-08-23 10:20 cmarche Note Added: 0003419
2012-08-23 10:30 boris Note Added: 0003420
2012-08-23 10:37 cmarche Note Added: 0003421
2012-08-23 10:41 cmarche Status assigned => resolved
2012-08-23 10:41 cmarche Resolution open => fixed
2013-03-27 09:43 signoles Note Added: 0003778
2013-03-27 09:44 signoles Fixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44 signoles Status resolved => closed
+Issue History