Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001828Frama-CPlug-in > wppublic2014-07-08 14:262015-03-17 22:18
Reportercorrenson 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001828: Frame Validity
Description//@ requires \valid(one);
void f(int *one){
   int two;
   //@ assert one != &two;
}

int *zero;
//@ requires \valid(zero) && \valid(one);
void frame(int *one, int arg){
   int two;
   //@ assert formal: \separated(one,&arg,&two);
   //@ assert global: \separated(zero,&arg,&two);
}
TagsNo tags attached.
Attached Files? file icon bts1828_frame.i [^] (197 bytes) 2014-08-21 10:19 [Show Content]

- Relationships

-  Notes
(0005409)
patrick (developer)
2014-08-21 09:12
edited on: 2014-08-21 10:20

 The initial issue was bettween locals and formals.
The same kind of problem exists between locals and globals, and between formals and globals...
So the example of description was extended.
(0005455)
patrick (developer)
2014-09-15 10:11

 Fix committed to master branch.

- Issue History
Date Modified Username Field Change
2014-07-08 14:26 correnson New Issue
2014-07-08 14:26 correnson Status new => assigned
2014-07-08 14:26 correnson Assigned To => correnson
2014-08-21 09:07 patrick Description Updated View Revisions
2014-08-21 09:12 patrick Note Added: 0005409
2014-08-21 09:53 patrick Description Updated View Revisions
2014-08-21 09:55 patrick Note Edited: 0005409 View Revisions
2014-08-21 10:12 patrick Description Updated View Revisions
2014-08-21 10:18 patrick Description Updated View Revisions
2014-08-21 10:19 patrick File Added: bts1828_frame.i
2014-08-21 10:20 patrick Note Edited: 0005409 View Revisions
2014-09-15 10:11 patrick Note Added: 0005455
2014-09-15 10:11 patrick Assigned To correnson => patrick
2014-09-15 10:11 patrick Status assigned => resolved
2014-09-15 10:11 patrick Resolution open => fixed
2014-10-31 09:55 correnson Relationship added related to 0001669
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker