unsoundness of Jessie with respect to expression evaluation of ANSI-C
ID0000289: This issue was created automatically from Mantis Issue 289. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000289 | Frama-C | Plug-in > jessie | public | 2009-10-19 | 2010-06-09 |
| Reporter | Sylvain Boulme | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | - |
Description :
The following program is completely proved by Jessie (using Alt-Ergo 0.9). However, when compiled with gcc on my Linux-PC, it leads to a segmentation fault.
The problem seems to come from the fact that Jessie chooses an order of evaluation for subexpressions which is different from my gcc. Actually ANSI-C specifies that the order of evaluation is indeterminate.
Some hints to fix this problem:
- detect and forbids expressions which depend on evaluation order.
- alternatively, emulate the semantics of x = c - decr() by if (anybool()) { tmp_l=c ; tmp_r=decr() ; } else { tmp_r=decr(); tmp_l=c ; } x = tmp_l - tmp_r ;
where anybool is simply declared as:
/*@ assigns \nothing ; */ int anybool () ;
However, this last approach may lead to an explosion of proof obligations.