2021-01-21 05:26 CET

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


There are no notes attached to this issue.

-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