Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #839

Closed
Open
Created Oct 30, 2014 by Jochen Burghardt@burghardt

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

  • 050.cpp
  • 050a.cpp
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking