Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001686Frama-CPlug-in > wppublic2014-03-12 16:542017-03-14 08:58
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001686: Provide an option to run Coq from Frama-C
DescriptionWhen proving external Coq-lemma for WP it might be interesting to run Coq from Frama-C, e.g.,

      frama-c -wp-coq Foo.v
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006382)
jens (reporter)
2017-03-13 16:18

I have to admit that I don't fully understand this issue anymore.
I suggest to close it.

- Issue History
Date Modified Username Field Change
2014-03-12 16:54 jens New Issue
2014-03-12 16:54 jens Status new => assigned
2014-03-12 16:54 jens Assigned To => correnson
2017-03-13 16:18 jens Note Added: 0006382
2017-03-14 08:58 yakobowski Status assigned => closed
2017-03-14 08:58 yakobowski Resolution open => no change required


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker