Skip to content

local array decl with non-constant size causes Why error

ID0000416: This issue was created automatically from Mantis Issue 416. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000416 Frama-C Plug-in > jessie public 2010-02-22 2010-02-22
Reporter Jochen Assigned To cmarche Resolution open
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Beryllium-20090902 Target Version - Fixed in Version -

Description :

After 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).

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information