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
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusconfirmedResolutionopen 
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
(0006514)
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 - 2018 MantisBT Team
Powered by Mantis Bugtracker