Generate out-of-scope variable when using quantified variable in a \old
ID0001762: This issue was created automatically from Mantis Issue 1762. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001762 | Frama-C | Plug-in > E-ACSL | public | 2014-04-25 | 2018-11-30 |
| Reporter | signoles | Assigned To | fmaurica | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | Frama-C 18-Argon | Fixed in Version | Frama-C 18-Argon |
Description :
===== a.i ===== /*@ ensures \forall integer i; 0 <= i < 10 ==> \old(t[i]) == 0; */ void f(int *t) { }
int main(void) { int t[10]; int i; for(i = 0; i < 10; i++) t[i] = 0; f(t); return 0; }
$ frama-c a.i -e-acsl -then-on e-acsl -print -ocode res.i $ ./gcc.sh res.i compiling res.i res.i: In function ‘__e_acsl_f’: res.i:84:53: error: ‘__e_acsl_i’ undeclared (first use in this function) res.i:84:53: note: each undeclared identifier is reported only once for each fun