Skip to content
GitLab
Projects Groups Snippets
  • /
  • 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 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1045
Closed
Open
Issue created May 01, 2014 by Jens Gerlach@gerlach

Unproven rte assertions for bit complement

ID0001769: This issue was created automatically from Mantis Issue 1769. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001769 Frama-C Plug-in > RTE public 2014-05-01 2014-05-19
Reporter jens Assigned To correnson Resolution no change required
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version -

Description :

I am struggling with unproven run time assertions in a some piece of code that heavily relies on bit operations. In fact, I am not sure this an issue of the rte plug-in. It is probably related to https://bts.frama-c.com/view.php?id=1750 which I submitted to the WP section. However, I wonder if the rte plug-in could make the task of WP easier.

The attached file simply performs bitwise complement for various unsigned integer types. For unsigned char and unsigned short the rte plugin generates unsigned_downcast assertion that WP cannot discharge. I understand that the promotion of the variable "a" to int is covered by the C standard. On the other hand, the C standard says in 6.5.3.4 (4)

   If the promoted type is an unsigned type, the expression ~E is equivalent to the maximum value  
   representable in that type minus E.

So, no overflow will occur.

Steps To Reproduce :

I called the file with the following options

frama-c-gui.byte -cpp-command 'gcc -C -E -nostdinc -I/usr/local/share/frama-c/libc' -pp-annot -no-unicode -wp -warn-signed-downcast -warn-signed-overflow -warn-unsigned-downcast -warn-unsigned-overflow -wp-rte complement.c

Attachments

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