Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002349Frama-CPlug-in > clangpublic2018-01-31 14:442018-01-31 15:19
Assigned Tovirgile 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002349: warning from kernel about exceptions
DescriptionThis 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?
TagsNo tags attached.
Attached Filescpp file icon exception_warning.cpp [^] (161 bytes) 2018-01-31 14:44
cpp file icon exception_warning_noexcept.cpp [^] (170 bytes) 2018-01-31 14:45

- Relationships

-  Notes
virgile (developer)
2018-01-31 15:18
edited on: 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.

- Issue History
Date Modified Username Field Change
2018-01-31 14:44 jens New Issue
2018-01-31 14:44 jens Status new => assigned
2018-01-31 14:44 jens Assigned To => virgile
2018-01-31 14:44 jens File Added: exception_warning.cpp
2018-01-31 14:45 jens File Added: exception_warning_noexcept.cpp
2018-01-31 15:18 virgile Note Added: 0006514
2018-01-31 15:18 virgile Note Edited: 0006514 View Revisions
2018-01-31 15:19 virgile Severity minor => feature
2018-01-31 15:19 virgile Status assigned => confirmed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker