Frama-C sleeps too much when discharging trivial goals
ID0002280: This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002280 | Frama-C | Plug-in > wp | public | 2017-02-13 | 2017-02-14 |
| Reporter | pkhuong | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | tweak | Reproducibility | always |
| Platform | Linux/x86_64 | OS | Linux | OS Version | 4.9.0-1-amd64 #1 |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
I have a largish C functions that generates ~70K goals (that I'm refactoring away). Verification with WP and RTE assertions succeeds, but takes ~14 minutes of real time. strace shows the majority of that time is spent executing no syscall (i.e., not calling external solvers) except printing the progress on stderr, getrusage, and nanosleeping for half a second. I LD_PRELOADed a shared object to turn usleep into a no-op, and that improved the runtime from 14 minutes to 3 minutes.
Could Frama-C sleep less when Qed does all the work?
Steps To Reproduce :
frama-c slow_qed.c -cpp-gnu-like -no-asm-contracts -constfold -machdep x86_64 -implicit-function-declaration error -wp -wp-rte -wp-extensional -wp-split -wp-init-const -wp-prop="-trustme,-freeable,-@assigns,-@lemma,-@variant" -wp-prover=alt-ergo,Z3:4.5.0