2021-01-27 11:25 CET
  

View Issue Details [ Jump to Notes ] [ 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 
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 - 
    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);
}
    ? file icon bts1828_frame.i (197 bytes) 2014-08-21 10:19 +

-Relationships
+Relationships

-Notes

~0005409

patrick (developer)

2014-08-21 09:12

Last edited: 2014-08-21 10:20

View 3 revisions

 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.
+Notes

-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 correnson Source_changeset_attached => framac master 7a6aae68
2014-09-15 10:11 patrick Source_changeset_attached => framac master 9c44791c
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
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed
+Issue History