View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001291 | Frama-C | Kernel > ACSL implementation | public | 2012-10-26 16:52 | 2012-10-31 11:38 | ||||||||
Reporter | cmarche | ||||||||||||
Assigned To | virgile | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | acknowledged | Resolution | open | ||||||||||
Product Version | Frama-C Oxygen-20120901 | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001291: Typing rejects polymorphic logic constants | ||||||||||||
Description | The followingACSL declaration should be valid axiomatic Bag { type bag<X>; logic bag<X> empty<X>; } 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. | ||||||||||||
Additional Information | 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... | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|