Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001694Frama-CPlug-in > wppublic2014-03-13 17:052014-03-13 17:05
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001694: Generate proof obligation for drivers when driver instantiate a logic acsl declaration
DescriptionThis would be helpful for proving (in coq) that a model of an ACSL logic function actually exists.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-03-13 17:05 jens New Issue
2014-03-13 17:05 jens Status new => assigned
2014-03-13 17:05 jens Assigned To => correnson

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker