Slow in proof obligation generation
ID0002156: This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002156 | Frama-C | Plug-in > wp | public | 2015-09-03 | 2015-09-07 |
| Reporter | juki21c | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | Both Ubuntu and OS X | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
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.
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