Frama-C Bug Tracking System - Frama-C
View Issue Details
0000967Frama-CKernel > ACSL implementationpublic2011-09-19 15:462012-02-09 19:26
Mihaela Sighireanu 
normalminorhave not tried
Frama-C Carbon-20110201 
0000967: unbound function \length in annotation
It seems that the function \length cannot be used with logic array types, e.g.: /*@ type node = int[]; */ /*@ predicate ls(node n) = @ \length(n) >= 1 ; */ returns after frama-c -typecheck [kernel] user error: unbound function \length in annotation
No tags attached.
Issue History
2011-09-19 15:46Mihaela SighireanuNew Issue
2011-09-19 15:46Mihaela SighireanuStatusnew => assigned
2011-09-19 15:46Mihaela SighireanuAssigned To => virgile

There are no notes attached to this issue.