Failure to record global variable with initialiser
ID0002194: This issue was created automatically from Mantis Issue 2194. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002194 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2019-01-25 |
| Reporter | kvorobyov | Assigned To | signoles | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
/* 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; }
Additional Information :
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.