Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000967Frama-CKernel > ACSL implementationpublic2011-09-19 15:462012-02-09 19:26
ReporterMihaela Sighireanu 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000967: unbound function \length in annotation
DescriptionIt 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-09-19 15:46 Mihaela Sighireanu New Issue
2011-09-19 15:46 Mihaela Sighireanu Status new => assigned
2011-09-19 15:46 Mihaela Sighireanu Assigned To => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker