| 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 |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
| There are no notes attached to this issue. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2012-10-26 16:52 | cmarche | New Issue | |
| 2012-10-26 16:52 | cmarche | Status | new => assigned |
| 2012-10-26 16:52 | cmarche | Assigned To | => virgile |
| 2012-10-31 11:38 | virgile | Status | assigned => acknowledged |
| Issue History |