use of "new" causes warning
ID0001945: This issue was created automatically from Mantis Issue 1945. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001945 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-02-17 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | text | Reproducibility | always |
| Platform | frama-c-Neon-20140301+dev-stance | OS | xubuntu-cfe13.10 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
running file 050.cpp (from the resolved issue #1569 (closed)) generates the output:
Now output intermediate result [kernel] warning: Assuming declared function malloc can't throw any exception
In the long run, this warning should be avoided, since it is confusing to novel users. All methods (such as malloc) that don't originate from C++ user input should be handled as known to Frama-C.
According to Stroustrup's "The C++ programming language" (3rd ed.), sect.14.10, "new" may throw the exception "bad_alloc". Frama-C should be aware of this, without telling it to the user every time.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information