Frama-C Bug Tracking System - Frama-C
View Issue Details
0001251Frama-CPlug-in > jessiepublic2012-07-31 10:532013-03-27 09:44
boris 
cmarche 
normalmajoralways
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001251: Binary search doesn't verify anymore after upgrade
After 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.
No tags attached.
c mismatch.c (699) 2012-07-31 10:53
https://bts.frama-c.com/file_download.php?file_id=411&type=bug
c binary-search.c (1,190) 2012-08-20 20:27
https://bts.frama-c.com/file_download.php?file_id=417&type=bug
html bts1251.html (10,998) 2012-08-21 13:30
https://bts.frama-c.com/file_download.php?file_id=418&type=bug
png gWhy.png (281,751) 2012-08-21 15:05
https://bts.frama-c.com/file_download.php?file_id=420&type=bug
? .why3.conf (1,358) 2012-08-21 18:18
https://bts.frama-c.com/file_download.php?file_id=421&type=bug
? .whyrc (458) 2012-08-21 18:19
https://bts.frama-c.com/file_download.php?file_id=422&type=bug
? why3.conf (327) 2012-08-22 13:27
https://bts.frama-c.com/file_download.php?file_id=423&type=bug
html binary-search.html (3,117) 2012-08-22 20:36
https://bts.frama-c.com/file_download.php?file_id=424&type=bug
Issue History
2012-07-31 10:53borisNew Issue
2012-07-31 10:53borisStatusnew => assigned
2012-07-31 10:53borisAssigned To => cmarche
2012-07-31 10:53borisFile Added: mismatch.c
2012-08-20 14:06cmarcheNote Added: 0003401
2012-08-20 20:27borisFile Added: binary-search.c
2012-08-20 20:28borisNote Added: 0003403
2012-08-21 13:30cmarcheFile Added: bts1251.html
2012-08-21 13:31cmarcheNote Added: 0003404
2012-08-21 13:35cmarcheNote Added: 0003405
2012-08-21 15:05borisNote Added: 0003407
2012-08-21 15:05borisFile Added: gWhy.png
2012-08-21 15:58cmarcheNote Added: 0003408
2012-08-21 18:18borisNote Added: 0003409
2012-08-21 18:18borisFile Added: .why3.conf
2012-08-21 18:19borisFile Added: .whyrc
2012-08-22 12:41cmarcheNote Added: 0003411
2012-08-22 13:27borisFile Added: why3.conf
2012-08-22 13:47cmarcheNote Added: 0003412
2012-08-22 14:35borisNote Added: 0003413
2012-08-22 16:31cmarcheNote Added: 0003414
2012-08-22 16:58cmarcheNote Edited: 0003414
2012-08-22 17:09borisNote Added: 0003415
2012-08-22 17:38cmarcheNote Added: 0003416
2012-08-22 17:44cmarcheNote Added: 0003417
2012-08-22 20:36borisFile Added: binary-search.html
2012-08-22 20:39borisNote Added: 0003418
2012-08-23 10:20cmarcheNote Added: 0003419
2012-08-23 10:30borisNote Added: 0003420
2012-08-23 10:37cmarcheNote Added: 0003421
2012-08-23 10:41cmarcheStatusassigned => resolved
2012-08-23 10:41cmarcheResolutionopen => fixed
2013-03-27 09:43signolesNote Added: 0003778
2013-03-27 09:44signolesFixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44signolesStatusresolved => closed

Notes
(0003401)
cmarche   
2012-08-20 14:06   
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.
(0003403)
boris   
2012-08-20 20:28   
Sorry, this is the binary search file.
(0003404)
cmarche   
2012-08-21 13:31   
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.
(0003405)
cmarche   
2012-08-21 13:35   
By the way, you could send your own results by sending the .xml file that is located in binary-search.jessie/binary-search/why3session.xml note that the html file can be generated using why3session html binary-search.jessie/binary-search resulting in a file binary-search.jessie/binary-search/binary-search.html
(0003407)
boris   
2012-08-21 15:05   
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 ~/progs/c/frama-c/binary-search$ Therefore, I can't generate an html-file: ~/progs/c/frama-c/binary-search$ why3session html binary-search.jessie/binary-search anomaly: Not_found
(0003408)
cmarche   
2012-08-21 15:58   
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" ?
(0003409)
boris   
2012-08-21 18:18   
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.
(0003411)
cmarche   
2012-08-22 12:41   
I am still trying to understand the problem but no success yet. Please could you attach the following file ? /usr/local/lib/why/why3/why3.conf
(0003412)
cmarche   
2012-08-22 13:47   
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
(0003413)
boris   
2012-08-22 14:35   
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 <0.103804> [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* ./why/why3/jessie3_integer.why ./why/why3/jessie3.why ./why/why3/jessie3.mlw /usr/local/lib$ ocamlc -v The Objective Caml compiler, version 3.12.1 Standard library directory: /usr/lib/ocaml I use Debian 7.
(0003414)
cmarche   
2012-08-22 16:31   
(edited on: 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 ?
(0003415)
boris   
2012-08-22 17:09   
~/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
(0003416)
cmarche   
2012-08-22 17:38   
Then this shows that the problem is related to /usr/local/lib/why/why3/why3.conf Great! 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 [main] loadpath = " ..."
(0003417)
cmarche   
2012-08-22 17:44   
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
(0003418)
boris   
2012-08-22 20:39   
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).
(0003419)
cmarche   
2012-08-23 10:20   
The problem with main unproved is related to the weaknesses of Jessie regarding allocation. I guess you mean it was proved with Why2 before ?
(0003420)
boris   
2012-08-23 10:30   
Yes, all VCs in binary-search.c were proved with the previous version of Why2/Jessie and Alt-Ergo.
(0003421)
cmarche   
2012-08-23 10:37   
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 /usr/local/lib/why/why3/jessi3.mlw 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 !
(0003778)
signoles   
2013-03-27 09:43   
Fixed in Frama-C Oxygen + Why 2.32.