Frama-C Bug Tracking System - Frama-C
View Issue Details
0001694Frama-CPlug-in > wppublic2014-03-13 17:052014-03-13 17:05
jens 
correnson 
normalfeatureN/A
assignedopen 
Frama-C Neon-20140301 
 
0001694: Generate proof obligation for drivers when driver instantiate a logic acsl declaration
This would be helpful for proving (in coq) that a model of an ACSL logic function actually exists.
No tags attached.
Issue History
2014-03-13 17:05jensNew Issue
2014-03-13 17:05jensStatusnew => assigned
2014-03-13 17:05jensAssigned To => correnson

There are no notes attached to this issue.