Frama-C Bug Tracking System - Frama-C
View Issue Details
0001214Frama-CPlug-in > Evapublic2012-06-18 16:562014-02-12 16:58
Anne 
yakobowski 
normalminorhave not tried
closedfixed 
 
Frama-C Oxygen-20120901 
0001214: FRAMA_C_MALLOC_INFINITE not used in stdlib.c
#define FRAMA_C_MALLOC_INFINITE #include "stdlib.c" doesn't do what is expected since stdlib.c begins with : #ifndef FRAMA_C_MALLOC_HEAP #ifndef FRAMA_C_MALLOC_CHUNKS #ifndef FRAMA_C_MALLOC_INDIVIDUAL #ifndef FRAMA_C_MALLOC_POSITION #define FRAMA_C_MALLOC_HEAP so it ends up with FRAMA_C_MALLOC_HEAP instead. Is this on purpose ? PS. I select [Kernel] category because I don't know where else to put it...
No tags attached.
Issue History
2012-06-18 16:56AnneNew Issue
2012-06-18 17:06yakobowskiNote Added: 0003162
2012-06-18 17:06yakobowskiCategoryKernel => Plug-in > value analysis
2012-06-19 14:45yakobowskiNote Added: 0003172
2012-06-19 14:45yakobowskiAssigned To => yakobowski
2012-06-19 14:45yakobowskiStatusnew => assigned
2012-06-19 14:45svnCheckin
2012-06-19 14:45svnStatusassigned => resolved
2012-06-19 14:45svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:58yakobowskiNote Added: 0004654
2014-02-12 16:58yakobowskiStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0003162)
yakobowski   
2012-06-18 17:06   
Those implementations are only useful to Value for the moment.
(0003172)
yakobowski   
2012-06-19 14:45   
This is a bug, the first line should be #ifndef FRAMA_C_MALLOC_INFINITE Notice that FRAMA_C_MALLOC_INFINITE will no longer allocate an infinite memories (only very big ones).
(0004654)
yakobowski   
2014-02-12 16:58   
Fix committed to stable/neon branch.