Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000811Frama-CPlug-in > jessiepublic2011-05-02 19:512011-05-06 18:54
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000811: double struct dereferencing causes unbound variable error
DescriptionJessie reports <> for the attached program. Adding a "requires \valid(e)" makes the error message disappear. The code in the procedure body does not require the validity of e. It does not assign anything outside of e->next->next, so the "assigns" clause is overestimating, but correct. Therefor, Jessie should not report an error.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (145 bytes) 2011-05-02 19:51 [Show Content]

- Relationships

-  Notes
Jochen (reporter)
2011-05-06 18:51

Adding a "requires \valid(e)" does not help if two different struct types are involved. In file ftest2.c, the error remains if parameter e is declared as "struct _list", while it disappears if e is declared as "struct _elem".
Jochen (reporter)
2011-05-06 18:54

//here is file ftest2.c, mentioned in my previous note: struct _elem { struct _elem *next; }; struct _list { struct _elem *next; }; //@ requires \valid(e); assigns e->next->next; void push(struct _list* e) { //@ loop invariant 0; while (0) ; }

- Issue History
Date Modified Username Field Change
2011-05-02 19:51 Jochen New Issue
2011-05-02 19:51 Jochen Status new => assigned
2011-05-02 19:51 Jochen Assigned To => cmarche
2011-05-02 19:51 Jochen File Added: ftest.c
2011-05-06 18:51 Jochen Note Added: 0001851
2011-05-06 18:54 Jochen Note Added: 0001852

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker