normalization of "assigns" in statement contract doens't cope with introduced auxiliary variables
ID0002102: This issue was created automatically from Mantis Issue 2102. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002102 | Frama-Clang | Plug-in > wp | public | 2015-04-09 | 2015-06-29 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | sometimes |
| Platform | Sodium-20150201 (opam) | OS | xubuntu14.04 | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp 468.c" on the attached program generates an unprovable obligation (viz. "false" in Alt-Ergo's .mlw file) for the "assert" (statement contract) in line 7.
Running "frama-c-gui -wp 468.c" shows that the code normalization introduced an auxiliary variable "tmp", which is assigned, too (cf. attached image "468.gif"). However the "assigns" clause wasn't extended accordingly; so in the normalized version, the statement contract is indeed false.
A workaround, found by our student Timon Lapawczyk, is to enclose the statement in line 8 into braces, which makes the contract refer to a compound statement with "tmp" a hidden variable inside it. In this case, the statement contract is proven without problems.
