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] WP and incompatible casts

Hi,

This kind of code is normally not provable using WP, where all available memory models currently assume that data is always read or written with the same type.
In theory, we could also design a more general memory model, but it is terribly inefficient in practice and we have to implement memory portioning first.

By the way, you can play with the (unsound) model `Typed+cast` which allows heterogenous pointer casts, but with the following side conditions that you must check *by hand* :

« once a casted pointer (or union field) is written, it shall *never* be read again with a different type (or with different union field) »

When using Typed+casts, WP will warn you about casts to checked by hand (we don’t have warnings for unions yet, but they shall come soon).
	L.


> Le 26 juil. 2020 à 20:58, Tuttle, Mark <mrtuttle at amazon.com> a écrit :
> 
> Can you help me validate the following snippet of system code with Frama-C?
>  
> Please see the attached file foo.c (reproduced below), and try “frama-c -wp foo.c”. 
>  
> #include <stdint.h>
>  
> typedef struct {
>   unsigned id1;
>   unsigned id2;
> } header_t;
>  
> uint8_t buffer_data[100]; // normally allocated on the heap
>  
> void foo(){
>   uint8_t *buffer = buffer_data;
>   header_t *header = (header_t *)buffer;
>   //@ assert buffer == (uint8_t *)header;
>   return;
> }
>  
> It is common for system code to receive a buffer of bytes, and for those bytes to be interpreted as a header followed by data.  Frama-C considers the two casts (header_t *)buffer and (uint8_t *)header to be incompatible.  The first may be incompatible due to data alignment, but not the second.  And whether it is reasonable or not, it is allowed by compilers like gcc and routinely done.
>  
> The problem is that the assert seems unprovable.  It seems to become the goal “Prove: buffer at L1 = w_0.” where w_0 seems to be an unconstrained symbolic value.
>  
> Thanks,
> Mark
>  
>  
>  
>  
>  
>  
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200727/b7b8c4cb/attachment.html>