Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002280Frama-CPlug-in > wppublic2017-02-13 22:492017-02-14 08:40
Assigned Tocorrenson 
PlatformLinux/x86_64OSLinuxOS Version4.9.0-1-amd64 #1
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002280: Frama-C sleeps too much when discharging trivial goals
DescriptionI 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 Reproduceframa-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
TagsNo tags attached.
Attached Filesc file icon slow_qed.c [^] (6,953 bytes) 2017-02-13 22:49 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-02-13 22:49 pkhuong New Issue
2017-02-13 22:49 pkhuong Status new => assigned
2017-02-13 22:49 pkhuong Assigned To => correnson
2017-02-13 22:49 pkhuong File Added: slow_qed.c

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker