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
  • #298

Closed
Open
Created Nov 11, 2016 by Jochen Burghardt@burghardt

"pointer comparison" warning emitted for "p==NULL"

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


Id Project Category View Due Date Updated
ID0002256 Frama-C Plug-in > Eva public 2016-11-11 2017-12-17
Reporter Jochen Assigned To maroneze Resolution open
Priority normal Severity minor Reproducibility always
Platform - OS xubuntu OS Version -
Product Version Frama-C Aluminium Target Version Frama-C 15-Phosphorus Fixed in Version -

Description :

Running "frama-c -val -val-warn-undefined-pointer-comparison=pointer ptrcmp3.c" on the attached file results in a warning:

ptrcmp3.c:10:[kernel] warning: pointer comparison. assert \pointer_comparable((void *)p, (void *)0);

The warning disappears if

  1. the type of parameter "name" is changed from "char*" to "char" both in "foo" and in "main", or
  2. the "assigns" clause for "foo" is deleted.

The warning seems strange by itself, as every pointer should be comparable to NULL. The changes that make the warning disappear (in particular 1.) support the hypothesis that this is a bug.

Attachments

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