Frama-C Bug Tracking System - Frama-C
View Issue Details
0001693Frama-CPlug-in > wppublic2014-03-13 17:022014-03-14 13:22
jens 
correnson 
highfeatureN/A
assignedopen 
Frama-C Neon-20140301 
 
0001693: Generate footprint from reads clauses of logic declarations
It would be helpful if the reads clause of an axiomatic definition would be used to generate additional hypothesis for coq proofs.
No tags attached.
related to 0001698closed patrick Add remark about additional axioms for read clauses 
Issue History
2014-03-13 17:02jensNew Issue
2014-03-13 17:02jensStatusnew => assigned
2014-03-13 17:02jensAssigned To => correnson
2014-03-14 13:22signolesRelationship addedrelated to 0001698

There are no notes attached to this issue.