Slow in proof obligation generation
ID0002156: This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.
|Plug-in > wp
|Both Ubuntu and OS X
|Fixed in Version
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