Frama-C Bug Tracking System - Frama-C
View Issue Details
0002381Frama-CPlug-in > E-ACSLpublic2018-07-01 14:152018-07-12 08:25
evdenis 
signoles 
normalminoralways
closedno change required 
 
 
0002381: E-ACSL: vla handling
The code:
int main(void)
{
   int size = 10;
   int array[size];

   return 0;
}


a.out.frama.c:141: undefined reference to `__fc_vla_alloc'
a.out.frama.c:143: undefined reference to `__fc_vla_free'
collect2: error: ld returned 1 exit status
e-acsl-gcc: fatal error: fail to compile/link instrumented code
No tags attached.
duplicate of 0001834closed signoles Cannot compile variable length arrays 
Issue History
2018-07-01 14:15evdenisNew Issue
2018-07-01 14:15evdenisStatusnew => assigned
2018-07-01 14:15evdenisAssigned To => signoles
2018-07-01 14:41evdenisNote Added: 0006566
2018-07-11 15:59signolesNote Added: 0006584
2018-07-11 15:59signolesStatusassigned => feedback
2018-07-11 15:59signolesRelationship addedduplicate of 0001834
2018-07-11 16:00signolesNote Added: 0006585
2018-07-12 07:36evdenisNote Added: 0006586
2018-07-12 07:36evdenisStatusfeedback => assigned
2018-07-12 08:25signolesStatusassigned => closed
2018-07-12 08:25signolesResolutionopen => no change required

Notes
(0006566)
evdenis   
2018-07-01 14:41   
The bug may be the duplicate of 0001834.
(0006584)
signoles   
2018-07-11 15:59   
Which version do you use?

This issue has been reported in issue 1834 (https://bts.frama-c.com/view.php?id=1834 [^]) but it supposes to be fixed in the latest release (Chlorine).
(0006585)
signoles   
2018-07-11 16:00   
BTW I cannot reproduce it with the latest release.
(0006586)
evdenis   
2018-07-12 07:36   
Indeed, seems like I tested it on the previous release. Please, close the ticket.