Typing problem into the logic about C variable of an array type.

ID0000549: This issue was created automatically from Mantis Issue 549. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000549	Frama-C	Kernel > ACSL implementation	public	2010-07-28	2014-02-12

Reporter	patrick	Assigned To	virgile	Resolution	fixed
Priority	high	Severity	major	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	Frama-C Carbon-20101201-beta1

Description :

Some times, the inferred type is T* instead of T[].

In the given exemple, the current version of Frama-C (Revision: 9458) both arguments of == operator used into the assert clause have type int* instead of int[10]

Additional Information :

int t1[10], t2[10] ;

int main () { int i ; for (i=0 ; i < 10 ; i++) t1[i] = 0 ; t2[i] = 0 ; } if (t1 == t2) { /* C tests the address of the first elements, * so the then-branch is dead. / //@ assert false; } else { / ACSL tests the contents of the arrays, * here they are the same. */ //@ assert (t1==t2) ; // even with the previous C } }