Skip to content

GitLab

  • Menu
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 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
  • #787

Closed
Open
Created Apr 11, 2014 by Jens Gerlach@gerlach

Frama-C/WP fails to discharge simple bit operation for small integer types

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


Id Project Category View Due Date Updated
ID0001750 Frama-C Plug-in > wp public 2014-04-11 2015-03-17
Reporter jens Assigned To patrick Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version Frama-C Sodium

Description :

In the attached file there are for simple functions that computes

 b = a & 1;
 //@ assert b == 0 || b == 1;

where a and b are of type unsigned char, unsigned short, unsigned int and unsigned long.

Only for the types unsigned int and unsigned long cab WP (in fact QED) discharge the assertion. Both alt-ergo and CVC4 fail on unsigned char and unsigned short.

I would be very nice if Frama-C/WP could handle the other cases automatically as well.

Attachments

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