suggest to document Frama-C's handling of return value optimization
ID0002022: This issue was created automatically from Mantis Issue 2022. Further discussion may take place here.
|ID0002022||Frama-Clang||Plug-in > clang||public||2014-12-08||2015-02-15|
|Product Version||-||Target Version||-||Fixed in Version||-|
Running "frama-c -wp -wp-rte 192.cpp" on the attached program verifies all obligations, thus showing that Frama-C assumes that no return value optimization (RVO) is done (the copy constructor "X()" from line 13 is called once for the "return" in line 21, and a second time for the initialization in line 25; as a result, the digit "2" is appended to variable "s" twice).
I suggest that Frama-C prints a warning that it assumes that no RVO is done. The g++ compiler doesn't do this; however, Frama-C/Wp users are expected to be far more interested in semantic details than g++ users are. As an alternative, Frama-C's handling of RVO issues should eventually be explained in the manual.