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

[Akihisa Yamada]

Dear Le Ton Chanh,

> For example, our tool reports those two examples as non-terminating
> (NO) but the current expected results for them are YES.

I think I understand you, but also that the expected results are not
used in the competition (from Johannes's last mail).

Anyway, as Jürgen also agrees, I will correct "z = z++" to "z++" in

> 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

Best regards,
Akihisa

On 2015/07/21 15:12, Ton-Chanh Le wrote:
> Dear Yamada,
>
> If we consider "z = z++" as a typo, but we do not change
> neither this typo or the expected result, then we might report
> a correct answer as an unsound result.
>
> For example, our tool reports those two examples as non-terminating
> (NO) but the current expected results for them are YES.
>
> For those examples, to make them terminating, we have to fix
> the typo "z = z++;" to "z++;" or  "z = z + 1;"
>
> Best Regards,
>
> Le Ton Chanh
> Email: chanhle at comp.nus.edu.sg <http://comp.nus.edu.sg>
>
> On Tue, Jul 21, 2015 at 9:04 PM, Akihisa Yamada
> <akihisa.yamada at uibk.ac.at <mailto:akihisa.yamada at uibk.ac.at>> wrote:
>
>     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>
>         <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>
>         <mailto: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>
>         <mailto: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 <mailto: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/
>
>

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