Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000416Frama-CPlug-in > jessiepublic2010-02-22 19:442010-02-22 19:44
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000416: local array decl with non-constant size causes Why error
DescriptionAfter declaring in a procedure a local array of a size depending on some parameter, when I assert the range-validity, I get (a Kernel warning "No code for function __builtin_alloca" and) a Why error message "Unbound variable bitvector_alloc_table". This doesnt happen for a constant size (see attached file).
TagsNo tags attached.
Attached Filesc file icon localFlexArray01.c [^] (221 bytes) 2010-02-22 19:44 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-02-22 19:44 Jochen New Issue
2010-02-22 19:44 Jochen Status new => assigned
2010-02-22 19:44 Jochen Assigned To => cmarche
2010-02-22 19:44 Jochen File Added: localFlexArray01.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker