2021-01-24 23:25 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000998Frama-CPlug-in > Evapublic2011-11-02 12:54
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionno change required 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0000998: Invariant used only in absence of precondition
DescriptionIn the code below, analyzed using frama-c -val, the access *adr is proven valid only in the absence of requires.

/*@ requires count > 0; */
void bla(char * adr, int count) {
  //@ loop invariant \at(adr,Pre) <= adr < \at(adr,Pre)+\at(count,Pre);
  do {
    int v = *adr;
    adr++;
  } while (--count);
}

char t[42];

void main () {
  bla(t+28, 14);
}
TagsNo tags attached.
Attached Files

-Relationships
related to 0001006closedvirgile Kernel should desugar "complete behaviors" 
+Relationships

-Notes

~0002440

yakobowski (manager)

Last edited: 2011-11-02 12:54

Cannot reproduce as is. Adding behaviors exhibits the bug:

/*@ behavior pos: assumes count > 0; */
void bla(char * adr, int count) {
  //@ for pos: loop invariant \at(adr,Pre) <= adr < \at(adr,Pre)+\at(count,Pre);
  do {
    Frama_C_show_each(adr);
    int v = *adr;
    adr++;
  } while (--count);
}

char t[42];

void main () {
  bla(t+28, 14);
}

However, this is the expected behavior. Since pos is not necessarily the only possible behavior, we cannot reduce by it on the loop invariant. With a
"complete behaviors pos;" clause, the loop invariant is used as intended.

+Notes

-Issue History
Date Modified Username Field Change
2011-10-23 18:50 yakobowski New Issue
2011-10-23 18:50 yakobowski Status new => assigned
2011-10-23 18:50 yakobowski Assigned To => pascal
2011-10-23 18:50 yakobowski Assigned To pascal => yakobowski
2011-11-02 12:54 yakobowski Note Added: 0002440
2011-11-02 12:54 yakobowski Note Edited: 0002440
2011-11-02 12:54 yakobowski Status assigned => closed
2011-11-02 12:54 yakobowski Resolution open => no change required
2011-11-02 13:09 yakobowski Relationship added related to 0001006
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History