2021-01-21 05:26 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001291Frama-CKernel > ACSL implementationpublic2012-10-31 11:38
Reportercmarche 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in Version 
Summary0001291: 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...
TagsNo 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