Incorrect dependencies in presence of declared functions
ID0000993: This issue was created automatically from Mantis Issue 993. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000993 | Frama-C | Plug-in > from | public | 2011-10-20 | 2014-02-12 |
| Reporter | yakobowski | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
Consider the following code
//@ assigns *p \from \nothing; void f(int *p);
void main () { int x = 0; int y = 0;
f(&x); f(&y); }
Slicing the program on x results on keeping only y and the call f(&y), instead of the instructions related to x. (However, the result is correct with -calldeps.)