Frama-C-discuss mailing list archives

jean-baptiste.jeannin at hispano-suiza-sa.com (jean-baptiste.jeannin@hispano-suiza-sa.com) · Fri Nov 21 14:44:21 2008

Hi,

Thank you for your very detailed answer. It allows me to understand more 
deeply what is supported and what is not. And I am glad I can now 
understand my error message.

As for the casts between a union and an int I mentioned, I actually got 
confused. I wanted to mean: having both an int and a struct in a union; 
but you already answered in your first example beneath (the one with union 
U{int i; struct{short s1; short s2} s; }

Thank you,

Jean-Baptiste Jeannin

"Yannick Moy" <yannick.moy@gmail.com> 
21/11/2008 12:31

A
jean-baptiste.jeannin@hispano-suiza-sa.com
cc
frama-c-discuss@lists.gforge.inria.fr
Objet
Re: [Frama-c-discuss] Cast support with Jessie in Lithium

Hi,

Sorry I did not answer before. This question has already be partly 
answered off-line, but I summarize here what can be done with the Jessie 
plugin regarding unions and casts.

Unions without pointer fields are now translated to bitvectors, so that 
access in these unions are translated to low-level accesses. Thus, the 
following code can be analyzed, but we do not yet provide a way to prove 
the resulting assertions, by asserting that any subset of bits from the 
bitvector representation of 0 is 0:

union U {
  int i;
  struct { short s1; short s2; } s;
};

//@ requires \valid(x);
void zero(union U* x) {
  x->i = 0;
  //@ assert x->s.s1 == 0;
  //@ assert x->s.s2 == 0;
}

Unions with pointer fields (either direct fields or sub-fields of 
structure fields) are translated differently, because we treat pointers 
differently than other types, to allow an automatic analysis of separation 
of memory blocks. Thus, we treat unions with pointer fields as 
discriminated unions, so that writing in a field erases all information on 
other fields. This allows to verify the following program:

union U {
  int i;
  int* p;
};

//@ requires \valid(x);
void zero(union U* x) {
  x->i = 0;
  //@ assert x->i == 0;
  x->p = (int*)malloc(sizeof(int));
  *x->p = 1;
  //@ assert *x->p == 1;
}

Finally, casts between pointer types are allowed, with the corresponding 
accesses to memory treated as low-level accesses to some bitvector. This 
allows to verify the safety of the following program:

//@ requires \valid(x);
void zero(int* x) {
  char *c = (char*)x;
  *c = 0;
  c++;
  *c = 0;
  c++;
  *c = 0;
  c++;
  *c = 0;
}

Regarding your error message, it refers to an internal structure created 
for unsigned int* pointers. This says that casts between pointers and 
non-pointers are not allowed in the Jessie plugin, as its documentation 
says.

http://frama-c.cea.fr/jessie.html

What are the casts of union to int that you mention ? Do you mean pointer 
to union to int ?

Cheers,
Yannick

On Tue, Nov 18, 2008 at 11:23 AM, <
jean-baptiste.jeannin@hispano-suiza-sa.com> wrote:

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." # 
_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Yannick

#
" 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/20081121/694229e1/attachment.html