Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002156Frama-CPlug-in > wppublic2015-09-03 03:312015-09-07 13:16
Assigned Tocorrenson 
PlatformOSBoth Ubuntu and OS XOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002156: Slow in proof obligation generation
DescriptionI 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.
Steps To Reproduce> 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
TagsNo tags attached.
Attached Fileszip file icon [^] (103,856 bytes) 2015-09-03 03:31

- Relationships

-  Notes
yakobowski (manager)
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.

- Issue History
Date Modified Username Field Change
2015-09-03 03:31 juki21c New Issue
2015-09-03 03:31 juki21c Status new => assigned
2015-09-03 03:31 juki21c Assigned To => correnson
2015-09-03 03:31 juki21c File Added:
2015-09-07 13:16 yakobowski Note Added: 0006024

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker