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
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000811: double struct dereferencing causes unbound variable error
DescriptionJessie reports <<File "why/ftest.why", line 371, characters 25-51: Unbound variable _elem_e_1_alloc_table>> 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
(0001851)
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".
(0001852)
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker