Frama-C Bug Tracking System - Frama-C
View Issue Details
0002194Frama-CPlug-in > E-ACSLpublic2015-12-04 12:012019-01-25 10:55
kvorobyov 
signoles 
normalminoralways
assignedopen 
 
 
0002194: Failure to record global variable with initialiser
/* The following example wrongly fails the assertion */
#include <inttypes.h>
char *B = "foo";

unsigned long ref() {
   return (intptr_t)B;
}

int main(int argc, char **argv) {
    char *ptr = (char*)ref();
    //@ assert \valid_read(ptr);
    return 0;
}
This seems to be the case where memory analysis incorrectly determines that global variable 'B' should not be modelled and therefore it is omitted from the instrumentation.
No tags attached.
Issue History
2015-12-04 12:01kvorobyovNew Issue
2015-12-04 12:01kvorobyovStatusnew => assigned
2015-12-04 12:01kvorobyovAssigned To => kvorobyov
2016-09-13 07:52signolesAssigned Tokvorobyov => signoles
2018-02-22 10:37signolesAssigned Tosignoles => fmaurica
2019-01-25 10:55signolesAssigned Tofmaurica => signoles

There are no notes attached to this issue.