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.
|ID0002102||Frama-Clang||Plug-in > wp||public||2015-04-09||2015-06-29|
|Platform||Sodium-20150201 (opam)||OS||xubuntu14.04||OS Version||-|
|Product Version||Frama-C Sodium||Target Version||-||Fixed in Version||-|
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.