0001190: __builtin_alloca - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001190

Frama-C

Kernel

public

2012-06-08 15:38

2012-06-09 16:04

Reporter

Anne

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Frama-C Nitrogen-20111001

Target Version

Fixed in Version

Summary

0001190: __builtin_alloca

Description

In a file with a local array which size in defined by a variable :
   float a[n];
I get :
   [kernel] warning: Variable-sized local variable a
which is ok. But then, when I use the value analysis, I get :
  [kernel] warning: No code for function __builtin_alloca,
                     default assigns generated
because the declaration has been translated in :
  __lengthofa = (unsigned int)n;
  a = (float *)__builtin_alloca(sizeof(*a) * __lengthofa);
which looks fine, but the question is :
shouldn't the assigns property be defined somewhere inside Frama-C for the builtin functions ?
As a workaround, what prototype and assigns should I write for this function.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0003069) yakobowski (manager) 2012-06-09 16:04	Within Value, __builtin_alloca should be stubbed by a malloc-like builtin. Some of the existing builtins in malloc.h could be used.

Issue History
Date Modified	Username	Field	Change
2012-06-08 15:38	Anne	New Issue
2012-06-08 17:31	signoles	Status	new => assigned
2012-06-08 17:31	signoles	Assigned To	=> virgile
2012-06-09 16:04	yakobowski	Note Added: 0003069