Frama-C Bug Tracking System - Frama-C
View Issue Details
0001623Frama-CPlug-in > wppublic2014-01-21 14:502014-03-13 15:57
jens 
correnson 
normaltweakalways
closedfixed 
Linux, OSX
Frama-C Fluorine-20130601 
Frama-C Neon-20140301 
0001623: Allow starting coq from Frama-C GUI also for proven obligations
Currently it is not possible to start the codide from the Frama-C GUI for a proof obligation that has already been proven by Coq. However, it would be desirable to do so in order to improve/refactor an already existing proof.
No tags attached.
Issue History
2014-01-21 14:50jensNew Issue
2014-01-21 14:50jensStatusnew => assigned
2014-01-21 14:50jensAssigned To => correnson
2014-01-21 16:24corrensonNote Added: 0004430
2014-01-21 16:24corrensonStatusassigned => acknowledged
2014-01-30 12:55corrensonNote Added: 0004467
2014-01-30 12:55corrensonStatusacknowledged => resolved
2014-01-30 12:55corrensonResolutionopen => fixed
2014-01-30 13:12corrensonNote Added: 0004468
2014-02-04 19:07corrensonNote Added: 0004480
2014-02-12 16:57corrensonNote Added: 0004536
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004430)
correnson   
2014-01-21 16:24   
Yes, I agree this would be a great feature. It should be available in next release ;-)
(0004467)
correnson   
2014-01-30 12:55   
Fix committed to feature/wp-gui branch.
(0004468)
correnson   
2014-01-30 13:12   
Fix committed to master branch.
(0004480)
correnson   
2014-02-04 19:07   
Fix committed to feature/bug_1598 branch.
(0004536)
correnson   
2014-02-12 16:57   
Fix committed to stable/neon branch.