2021-03-02 03:16 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001302Frama-CPlug-in > Evapublic2012-11-14 09:242013-04-19 11:05
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001302: Crash with Invalid argument for Frama_C_alloc_size function
Description$ frama-c toto.c -val
gives :
[value] user error: Invalid argument for Frama_C_alloc_size function
(...)
         Unexpected error (Kernel_function.No_Definition).
         Please report as 'crash' at http://bts.frama-c.com/.

It seems ok that the value analysis doesn't know what to do with this example,
but I guess it shouldn't 'crash'...
TagsNo tags attached.
Attached Files
  • c file icon toto.c (189 bytes) 2012-11-14 09:24 - 
    #include <stdlib.h>

extern void*Frama_C_alloc_size(size_t);

void *malloc(size_t size) { return Frama_C_alloc_size(size); }

int main (int size) { int * p = malloc (size * sizeof(int)); }
    c file icon toto.c (189 bytes) 2012-11-14 09:24 +

-Relationships
+Relationships

-Notes

~0003537

yakobowski (manager)

2012-11-18 14:36

 Already fixed in the trunk.
+Notes

-Issue History
Date Modified Username Field Change
2012-11-14 09:24 Anne New Issue
2012-11-14 09:24 Anne Status new => assigned
2012-11-14 09:24 Anne Assigned To => pascal
2012-11-14 09:24 Anne File Added: toto.c
2012-11-18 14:20 yakobowski Assigned To pascal => yakobowski
2012-11-18 14:36 yakobowski Note Added: 0003537
2012-11-18 14:36 yakobowski Status assigned => resolved
2012-11-18 14:36 yakobowski Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History