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 204
    • Issues 204
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & 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
  • #1584
Closed
Open
Created Jul 16, 2009 by Fabrice Derepas@fderepas

wrongly synthesized assert

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


Id Project Category View Due Date Updated
ID0000195 Frama-C Plug-in > Eva public 2009-07-16 2014-02-12
Reporter derepas Assigned To pascal Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Beryllium-20090601-beta1 Target Version - Fixed in Version Frama-C Beryllium-20090901

Description :

Let's consider the following program:

  1. #include <stdlib.h>
  2. struct my_struct {
  3. void * my_field;
  4. };
  5. void main(struct my_struct * l) {
  6. if (l!=NULL) {
  7. if (l->my_field!=NULL) {
  8.   l->my_field=NULL;
  9. }
  10. }
  11. } Then I launch frama-c-gui and value analysis on entry point 'main'. The following assert is synthesized between line 8 and 9: //@ assert \valid(&l->my_field); Even though l->my_field could be NULL and the program be ok.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking