11 if-statements lead to why-runtime >12 min
ID0000688: This issue was created automatically from Mantis Issue 688. Further discussion may take place here.
|ID0000688||Frama-C||Plug-in > jessie||public||2011-01-25||2011-01-26|
|Reporter||Jochen||Assigned To||cmarche||Resolution||no change required|
|Product Version||Frama-C Boron-20100401||Target Version||-||Fixed in Version||-|
I tried to test whether "why" builds one proof obligation per relevant program-path, came up with the attached program to cause a combinatorial explosion, and succeeded. I guess, this problem is unavoidable.
However, I'd expected "why" to be able to cope with at least 2^16 paths, rather than <2^11 only. There might be programs of practical relevance with a variable's value at some program point depending of that much case distinctions.
Maybe the manual should recommend for such programs the use of intermediate assert-clause, like "assert (y & 0xff) == (x & 0xff)" between line 10 and 11 in ftest.c.