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,

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081121/7968c584/attachment.html