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
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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
(0003401)
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.
(0003403)
boris (reporter)
2012-08-20 20:28

Sorry, this is the binary search file.
(0003404)
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.
(0003405)
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
(0003407)
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
(0003408)
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" ?
(0003409)
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.
(0003411)
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
(0003412)
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
(0003413)
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.
(0003414)
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

?

(0003415)
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
(0003416)
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 = " ..."
(0003417)
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
(0003418)
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).
(0003419)
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 ?
(0003420)
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.
(0003421)
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 !
(0003778)
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 - 2018 MantisBT Team
Powered by Mantis Bugtracker