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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000688 | Frama-C | Plug-in > jessie | public | 2011-01-25 | 2011-01-26 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | no change required |
| Priority | normal | Severity | text | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
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.