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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002022 | Frama-Clang | Plug-in > clang | public | 2014-12-08 | 2015-02-15 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | text | Reproducibility | always |
| Platform | frama-c-Neon-20140301+dev-stance | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
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.