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

[Akihisa Yamada]

Dear Ton-Chanh,

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

is this a request for the coming competition?

To me, it feels strange to change "Comment: terminating" line, which
seems to reflect the author's intention, rather than the apparent
typo "z = z++;".

May I leave them unchanged this time, since your request should not
affect the competition result?

Best regards,
Akihisa

On 2015/07/21 9:21, Ton-Chanh Le wrote:
> 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 <http://comp.nus.edu.sg>
>
> On Tue, Jul 21, 2015 at 2:14 PM, Andreas Gebhardt
> <andreasgebhardt at web.de <mailto: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 <mailto:Termtools at lists.lri.fr>
>     http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>
>
>
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>

-- 
Akihisa Yamada, Ph.D.
Computational Logic Group, Institute of Computer Science,
University of Innsbruck
http://cl-informatik.uibk.ac.at/~ayamada/