| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001302 | Frama-C | Plug-in > Eva | public | 2012-11-14 09:24 | 2013-04-19 11:05 |
|
| Reporter | Anne | |
| Assigned To | yakobowski | |
| Priority | normal | Severity | crash | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Oxygen-20120901 | |
| Target Version | | Fixed in Version | Frama-C Fluorine-20130401 | |
|
| Summary | 0001302: 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'... |
| Tags | No tags attached. |
|
| Attached Files |  toto.c [^] (189 bytes) 2012-11-14 09:24 [Show Content] [Hide Content]#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)); }
|
|
Relationships 
Relationships