Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000712Frama-CPlug-in > jessiepublic2011-02-10 12:132011-02-10 12:13
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in Version 
Summary0000712: Validity of valid pointer to struct member cannot be verified
DescriptionJessie is unable to verify that &this->v is valid in the code below.
Additional Informationtypedef struct { int v; } A; //@ requires \valid(this); void bar(int* this); //@ requires \valid(this); void foo(A* this) { bar(&this->v); // fails to verify }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-02-10 12:13 boris New Issue
2011-02-10 12:13 boris Status new => assigned
2011-02-10 12:13 boris Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker