Skip to content

Frama-C runs out of memory on small C program (combinatorial explosion in analysis of "main"?)

ID0002189: This issue was created automatically from Mantis Issue 2189. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002189 Frama-C Plug-in > wp public 2015-12-03 2015-12-03
Reporter Jochen Assigned To correnson Resolution open
Priority normal Severity tweak Reproducibility always
Platform Sodium-20150201 OS - OS Version xubuntu14.04
Product Version Frama-C Sodium Target Version - Fixed in Version -

Description :

Running "frama-c -wp -wp-rte -wp-prover none 10g.c" on the attached program causes Frama-C to run out of memory after allocation of 3 GBytes memory (deliberately restricted by "ulimit -v 3000000" to avoid swapping/paging).

This phenomenon disappears e.g. if

  • "main" is renamed to "foo" in line 28,
  • both "p1" and "p2" are made "static" in line 23,24, or
  • field "e0" or "e1" is removed from the "struct S" definition in line 9,14, and its use in line 33/34 is also removed.

Probably, there is some combinatorial explosion effect in the analysis. While this isn't a real bug, it may be worthwile to look after it, since the circumstances under which it can be observed are quite strange.

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information