value analysis memory consumption problem when using -lib-entry option
ID0001026: This issue was created automatically from Mantis Issue 1026. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001026 | Frama-C | Plug-in > Eva | public | 2011-11-25 | 2012-09-19 |
| Reporter | pherrmann | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | Frama-C Oxygen-20120901 | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
When calling the value analysis with the -lib-entry option, on a program declaring a big static array, the computation of the initial state consumes an huge amount of memory (Out of memory exception likely).
For instance, try
frama-c -lib-entry -main f ./f.c -val
on
char mem[100000000];
int f(int x) { return x; }
Additional Information :
svn around 16000 (but not a very recent bug)