Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Cast support with Jessie in Lithium

Hi,

When I was using Helium, I was told that pointer cast was not implemented 
at all yet but that it would (at least mostly) be fixed with the Lithium 
version. When I used the Lithium version I saw that lots of my pointer 
cast problems had disappeared, and I thank you for that.

However, I have no precise idea about which kind of pointer casts are 
supported and how they are supported (since for example, casting a float* 
to an int* can give a different result on different architectures). Could 
you please tell us precisely which kind of pointer casts (and other casts) 
are supported and which are not; I am particularly interested by:
- casts of union to int and vice-versa (this seems to be fully supported 
now, as far as I can see).
- casts of int to int* and vice-versa (since we do embedded software, a 
lot of addresses are written in the code and interpreted as int, and then 
casted to int* or float*)
- casts of (type1*) to (type2*) and vice-versa.

In particular, I got a strange error message which didn't catch my 
attention at first but does so now:

file.c:69: Error: Casting from type unsigned long to type struct 
unsigned_int_P * not allowed

It is particularly strange since I have never defined any type called 
unsigned_int_P, and (all my files being in the same directory), calling 
the command "grep unsigned\_int\_P *" gives no result. So, how should I 
interpret this error message?
Thank you,

Jean-Baptiste Jeannin

#
" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."

 " Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."
#
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081118/d065fedc/attachment.html