[Termtools] C category: x = x++ statements

[Ton-Chanh Le]

Dear Andreas Gebhardt,

Thank you very much for your clarification.

Your interpretation of x = x++

   x_ = x;
   x = x+1;
   x = x_;

is exactly the thing we received from cil.

According to this, I think we need to change
the expected results of

TPDB/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c
(non-terminating when x>y & y>x+z)

TPDB/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c
(non-terminating when x+y=0 & x+z=0 & x<=n)



Best Regards,

Le Ton Chanh
Email: chanhle at comp.nus.edu.sg

On Tue, Jul 21, 2015 at 2:14 PM, Andreas Gebhardt <andreasgebhardt at web.de>
wrote:

> Dear Ton-Chanh Le,
>
>  We have a problem with the x = x++ statements,
>> which appear in the examples
>>
>>
>> TPDB/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c
>>
>>
>>
>> TPDB/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c
>>
> >
>
>> [...]
>>
> >
>
>> Could we use x++ instead of x = x++ in those examples?
>>
>
> these two statements (together with a ';') are not interchangeable by
> default, the first statement
>
>         x++;
>
> increments the value of `x` and returns the value of `x` before it was
> incremented. The value which the statement returns is not used.
>   But the second one uses the return value of `x++`
>
>         x = x++;
>
> which is the value of `x` before it was incremented. So the value of `x`
> right before and right after the statement `x = x++;` does not change.
>
> Without using the postincrement operator (`x_` a fresh variable of same
> type as `x`)
>
>    x_ = x;
>    x = x+1;
>    x = x_;
>
>
> Best Regards,
> Andreas
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150721/f424f881/attachment.html>