Imprecision of 'Defs' when querying precise location
ID0001079: This issue was created automatically from Mantis Issue 1079. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001079 | Frama-C | Plug-in > scope | public | 2012-02-03 | 2014-02-12 |
| Reporter | yakobowski | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
typedef struct { int a; int b; } ts;
ts t[10];
void init() { t[1].a = 1; t[1].b = 2; }
unsigned int main () { init(); return t[1].a; }
Requiring the instructions that define t[1].a in main yields both lines of function init, which is a bit imprecise. Since slicing main on its return value removes the line 't[1].b = 2', the pdg is probably precise enough. Thus the imprecision lies somewhere in Scope.