| 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 | |
| Platform | | OS | | OS Version | |
| 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;
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.
|
| 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