GitLab

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)