GitLab

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