Slicer: slicing preserving some undesired function calls
ID0000107: This issue was created automatically from Mantis Issue 107. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000107 | Frama-C | Plug-in > slicing | public | 2009-05-27 | 2014-02-12 |
| Reporter | dpariente | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
(This issue was previously discussed through private messages but not yet resolved. It was noticed that a solution would require some "work around"! It is now recorded into the BTS for traceability reasons.)
The following code is sliced w.r.t. its annotation.
typedef struct { int i; int j; } las; las v1,v2,v3;
void g(las*p) { p->i = p->i * 2; }
void f() { g( &v1 ); g( &v2 ); g( &v3 ); //@ assert v2.i>=10; }
Command line: frama-c -slice-assert f -slice-print -lib-entry -main f foo.c
The sliced code got rid of the statement g(&v3) (with calldeps), but kept g(&v1). A slicer improvement would be, of course, to be able to get also rid of the 1st call to g (i.e., "g(&v1);")!