>unsigned long a;
>unsigned long *p;
>p = (unsigned long *)&p;
>a = ++(*p);
Gabriel, since p refers to itself this code looks to me like an
occurrence of the second clause of this type of undefined behavior:
"Between two sequence points, an object is modified more than once, or
Benjamin,
On Thu, Aug 27, 2009 at 07:49:18PM +0200, Benjamin Monate wrote:
> Indeed Frama-C is meant to be able to handle the case you mention.
> We had to preserve some informations about the possibly undefined
> behaviours coming from the original code. They one has to prove that
> these behavio
Hi,
Roberto Bagnara a écrit :
> Generally speaking, I wonder how the program verification
> tools based on CIL cope with this kind of problems (this
> is not the first such problem I report on the list).
> And this is relatively independent from the fact that the
> source program has fully defined
Gabriel Kerneis wrote:
> On Wed, Aug 26, 2009 at 11:30:47PM +0200, Roberto Bagnara wrote:
>>a = ++(*p);
>
> Are you sure the behavior of this line is defined in C? I don't how it
> could be incorrect to translate it to:
>(*p)++;
>a = *p;
> (which is precisely what CIL does).
Hi Gabrie
