Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001251Frama-CPlug-in > jessiepublic2012-07-31 10:532013-03-27 09:44
Assigned Tocmarche 
PlatformOSOS Version
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 Filesc file icon mismatch.c [^] (699 bytes) 2012-07-31 10:53 [Show Content]
c file icon binary-search.c [^] (1,190 bytes) 2012-08-20 20:27 [Show Content]
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

- Relationships

-  Notes
cmarche (developer)
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.
boris (reporter)
2012-08-20 20:28

Sorry, this is the binary search file.
cmarche (developer)
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.
cmarche (developer)
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
boris (reporter)
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
cmarche (developer)
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" ?
boris (reporter)
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.
cmarche (developer)
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
cmarche (developer)
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
boris (reporter)
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.
cmarche (developer)
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 ?
boris (reporter)
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
cmarche (developer)
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 = " ..."
cmarche (developer)
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
boris (reporter)
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).
cmarche (developer)
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 ?
boris (reporter)
2012-08-23 10:30

Yes, all VCs in binary-search.c were proved with the previous version of Why2/Jessie and Alt-Ergo.
cmarche (developer)
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 !
signoles (manager)
2013-03-27 09:43

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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker