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

[Ton-Chanh Le]

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

On Tue, Jul 21, 2015 at 9:04 PM, Akihisa Yamada <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>
>>
>> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150721/32244fa5/attachment.html>