Frama-C Bug Tracking System - Frama-C
View Issue Details
0002349Frama-CPlug-in > clangpublic2018-01-31 14:442018-01-31 15:19
0002349: warning from kernel about exceptions
This is more a question than a bug report... In the attached example Frama-Clang issue the warning frama-c -wp -wp-rte exception_warning.cpp [kernel] Parsing exception_warning.cpp (external front-end) Now output intermediate result [kernel] warning: Assuming declared function bar can't throw any exception This also occurs when I add "noexcept" to the declaration of "bar". (see second file: exception_warning_noexcept.cpp) Is there a way to declare in the contract that a function cannot throw? Or what do I have to do to get rid of this warning?
No tags attached.
cpp exception_warning.cpp (161) 2018-01-31 14:44
cpp exception_warning_noexcept.cpp (170) 2018-01-31 14:45
Issue History
2018-01-31 14:44jensNew Issue
2018-01-31 14:44jensStatusnew => assigned
2018-01-31 14:44jensAssigned To => virgile
2018-01-31 14:44jensFile Added: exception_warning.cpp
2018-01-31 14:45jensFile Added: exception_warning_noexcept.cpp
2018-01-31 15:18virgileNote Added: 0006514
2018-01-31 15:18virgileNote Edited: 0006514View Revisions
2018-01-31 15:19virgileSeverityminor => feature
2018-01-31 15:19virgileStatusassigned => confirmed

2018-01-31 15:18   
There is indeed currently no possibility to convey this information. Frama-Clang should reflect noexcept in the translated C code (probably as an attribute of the function), so that the exception analyzer could take this information into account.