Frama-C Bug Tracking System - Frama-C
View Issue Details
0001291Frama-CKernel > ACSL implementationpublic2012-10-26 16:522012-10-31 11:38
Frama-C Oxygen-20120901 
0001291: Typing rejects polymorphic logic constants
The followingACSL declaration should be valid axiomatic Bag { type bag; logic bag empty; } but is rejected by typing : [kernel] user error: some type variable appears only in the return type. All type variables need to occur also in the parameters types. in annotation.
I know it is annoying to implement since it requires a full-fledged type inference algorithm. But I don't see any way to avoid it...
No tags attached.
Issue History
2012-10-26 16:52cmarcheNew Issue
2012-10-26 16:52cmarcheStatusnew => assigned
2012-10-26 16:52cmarcheAssigned To => virgile
2012-10-31 11:38virgileStatusassigned => acknowledged

There are no notes attached to this issue.