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

[Juergen Giesl]

Dear all,

I also think that the best solution would be to change this typo in the
examples.

Best Regards
Juergen

2015-07-21 15:12 GMT+02:00 Ton-Chanh Le <chanhle at comp.nus.edu.sg>:

> 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/
>>
>
>
> _______________________________________________
> 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/fd4014d0/attachment.html>