Incorrect typing of annotations

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

---

Id	Project	Category	View	Due Date	Updated
ID0000570	Frama-C	Kernel > ACSL implementation	public	2010-08-24	2014-02-12

Reporter	monate	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	Frama-C Carbon-20101201-beta1

Description :

The following code should be accepted by Frama-C:

int main(char *data ) { //@ assert \pointer_comparable(data, (void *)0); return; }

but leads to "failure: Logic_typing.c_cast_to: char * -> void " Implicit promotion from char to void* is legal according to ACSL.