Gabriel Kerneis wrote:
> This is definitely a bug in CIL. I just stumbled upon the relevant part
> of the code and noticed that things are handled correctly in the case of
> simple assignments, but not for compound assignements (as you noticed).
>
> You will find a patch attached. Please, test i
Hi,
On Thu, Aug 27, 2009 at 12:03:15PM +0200, Roberto Bagnara wrote:
> Let us consider this example: [snip]
> 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).
This is definit
Gabriel Kerneis wrote:
> Disclaimer: I am not an expert, did not write CIL (neither gcc ;-), so
> what follows is nothing more than my humble understanding of C99.
Hi Gabriel.
> On Fri, Aug 28, 2009 at 06:00:40PM +0200, Enea Zaffanella wrote:
>> I was considering the second example sent by Robert
Disclaimer: I am not an expert, did not write CIL (neither gcc ;-), so
what follows is nothing more than my humble understanding of C99.
On Fri, Aug 28, 2009 at 06:00:40PM +0200, Enea Zaffanella wrote:
> I was considering the second example sent by Roberto.
> Here we need to evaluate the following
Enea Zaffanella wrote:
> Hello.
[...]
> I was considering the second example sent by Roberto.
[...]
> So I cannot see the undefined behavior mentioned in C99 6.5-2:
Could a CIL developer confirm whether or not my observations are
correct? That is, confirm whether or not this is a bug in CIL?
Che
Hello.
> On Fri, 2009-08-28 at 10:29 +0200, Benjamin Monate wrote:
>> AFAIU if p==&a then
>> a=++(*p) ;
>> is the same as
>> a=++a;
>> which is undefined as it has two effects on "a" between two sequence points.
>
> The example had p==&p, not p==&a. a=++(*p) doesn't have two effects on
> 'a'---it
On Fri, 2009-08-28 at 10:29 +0200, Benjamin Monate wrote:
> AFAIU if p==&a then
> a=++(*p) ;
> is the same as
> a=++a;
> which is undefined as it has two effects on "a" between two sequence points.
The example had p==&p, not p==&a. a=++(*p) doesn't have two effects on
'a'---it has one on 'a' and o
Gabriel Kerneis a écrit :
> Since you seem to have mastered the Standard far beyond what I managed,
> would you mind explaining why the behavior is indeed undefined in the
> cases discussed above? I read the relevant sections over and over for
> at least an hour and couldn't be convinced by either
John -
On Thu, Aug 27, 2009 at 04:59:45PM -0600, John Regehr wrote:
> >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 be
>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
13 matches
Mail list logo
