Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001693Frama-CPlug-in > wppublic2014-03-13 17:022014-03-14 13:22
Reporterjens 
Assigned Tocorrenson 
PriorityhighSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001693: Generate footprint from reads clauses of logic declarations
DescriptionIt would be helpful if the reads clause of an axiomatic definition would be used to generate additional hypothesis for coq proofs.
TagsNo tags attached.
Attached Files

- Relationships
related to 0001698closedpatrick Add remark about additional axioms for read clauses 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-03-13 17:02 jens New Issue
2014-03-13 17:02 jens Status new => assigned
2014-03-13 17:02 jens Assigned To => correnson
2014-03-14 13:22 signoles Relationship added related to 0001698


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker