Slicing does not preserve some ACSL constructs
ID0000690: This issue was created automatically from Mantis Issue 690. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000690 | Frama-C | Plug-in > slicing | public | 2011-01-26 | 2015-08-03 |
| Reporter | signoles | Assigned To | yakobowski | Resolution | not fixable |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20101202-beta2 | Target Version | - | Fixed in Version | - |
Description :
The slicer does not keep ACSL annotations if it does not understand them. This behavior may prevent to prove properties of the sliced program.
Steps To Reproduce :
Consider the following program: ==== a.c int t[10]; void main(void) { /*@ loop invariant 0 <= i <= 10; @ loop invariant \forall integer k; 0 <= k < i ==> t[k] == 0; @ / for(int i = 0; i < 10; i++) t[i] = 0; /@ assert t[0] == 0; */ }
Run it with: $ frama-c -slice-assert main -slice-print a.c The printed program forget the second loop invariant. Thus, for instance, plug-in WP cannot prove the final assertion anymore.
/* Generated by Frama-C / int t[10] ; void main(void) { { int i ; i = 0; /@ loop invariant (0 ? i) ? (i ? 10); */ while (i < 10) { t[i] = 0; i ++; } }
/*@ assert (t[0] ? 0); */ ; return; }