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: 0006514bug_revision_view_page.php?bugnote_id=6514#r335
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.