2021-01-22 19:59 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001623Frama-CPlug-in > wppublic2014-03-13 15:57
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSLinux, OSXOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001623: Allow starting coq from Frama-C GUI also for proven obligations
DescriptionCurrently 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.

TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0004430

correnson (manager)

Yes, I agree this would be a great feature. It should be available in next release ;-)

~0004467

correnson (manager)

Fix committed to feature/wp-gui branch.

~0004468

correnson (manager)

Fix committed to master branch.

~0004480

correnson (manager)

Fix committed to feature/bug_1598 branch.

~0004536

correnson (manager)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2014-01-21 14:50 jens New Issue
2014-01-21 14:50 jens Status new => assigned
2014-01-21 14:50 jens Assigned To => correnson
2014-01-21 16:24 correnson Note Added: 0004430
2014-01-21 16:24 correnson Status assigned => acknowledged
2014-01-30 12:55 correnson Source_changeset_attached => framac feature/wp-gui 83a88157
2014-01-30 12:55 correnson Note Added: 0004467
2014-01-30 12:55 correnson Status acknowledged => resolved
2014-01-30 12:55 correnson Resolution open => fixed
2014-01-30 13:12 correnson Source_changeset_attached => framac master cba1b159
2014-01-30 13:12 correnson Note Added: 0004468
2014-02-04 19:07 correnson Source_changeset_attached => framac feature/bug_1598 e1a03032
2014-02-04 19:07 correnson Note Added: 0004480
2014-02-12 16:53 correnson Source_changeset_attached => framac stable/neon cba1b159
2014-02-12 16:57 correnson Note Added: 0004536
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
+Issue History