Frama-C Bug Tracking System - Frama-C
View Issue Details
0002156Frama-CPlug-in > wppublic2015-09-03 03:312015-09-07 13:16
juki21c 
correnson 
normalminoralways
assignedopen 
Both Ubuntu and OS X
Frama-C Sodium 
 
0002156: Slow in proof obligation generation
I experienced that Frama-C/WP was very slow in generating the proof obligations only (skipping invoking any provers). For the attached files, code6.c takes about 1 min. code10.c takes about 15 min. code12.c abnormally terminates Frama-C with a stack overflow error.
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code6.c > frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code10.c > frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code12.c
No tags attached.
zip code.zip (103,856) 2015-09-03 03:31
https://bts.frama-c.com/file_download.php?file_id=1060&type=bug
Issue History
2015-09-03 03:31juki21cNew Issue
2015-09-03 03:31juki21cStatusnew => assigned
2015-09-03 03:31juki21cAssigned To => correnson
2015-09-03 03:31juki21cFile Added: code.zip
2015-09-07 13:16yakobowskiNote Added: 0006024

Notes
(0006024)
yakobowski   
2015-09-07 13:16   
Your functions are extremely long, because of the loop unrolling. This triggers at least one quadratic behavior in the parsing engine of Frama-C, and possibly some non-linear behaviors in the WP plugin. Notice that, with the current development version of Frama-C, I get not crash on any of the three files. However, this may just be related to different ulimit settings. Also, the the version of the Value plugin that will be available in Frama-C Magnesium will be able to prove all three examples. For your examples, that are almost completely deterministic, it might be a better fit than WP.