[Termtools] About memory examples in C category

[Thomas Ströder]

Dear Akihisa,

Could you update the one example where gcc shows the warning by the one
in the attachment?

Best regards,

  Thomas


Am 29.07.2015 um 17:08 schrieb Thomas Ströder:
> Dear all,
> 
> Since I did not get any further responses, I added the corresponding
> rules to http://www.termination-portal.org.
> 
> Best regards,
> 
>   Thomas
> 
> 
> Am 29.07.2015 um 03:25 schrieb Matthias Heizmann:
>> Hi Thomas,
>>
>>> Thoughts?
>> 1. I do not like rules that are complicated an difficult to explain.
>> 2. I like that we have a tool (gcc) that is able to check if a benchmark 
>> sticks to these rules.
>> 3. I do not like that we define our rule with respect to the output of a tool.
>> 4. I do not like what the man page of gcc says about Wsequence-point.
>> "Some more complicated cases are not diagnosed by this option, and it may give 
>> an occasional false positive result ..."
>>
>> However, I do not have a better idea and I expect that there is no perfect 
>> solution. Hence, I am in favor for using the proposed rule in this year's 
>> competition.
>>
>> Best,
>> Matthias
>>
>>
>> On Tuesday, July 28, 2015 14:48:20 Thomas Ströder wrote:
>>> Dear Akihisa,
>>>
>>> That sounds like a doable plan: We could disallow programs where gcc
>>> shows such a warning.
>>>
>>> How about this formulation of the rule:
>>>
>>> "Programs where the evaluation order of operations is not defined
>>> according to the C standard and where different execution orders of the
>>> operations lead to different resulting states are not allowed. As an
>>> example, the program
>>>
>>> int main(){
>>>      int x = 0;
>>>      while( x++ == x );
>>> }
>>>
>>> is not allowed since the evaluation order between ++ and == is not
>>> defined according to the C standard and if ++ is evaluated first, the
>>> program terminates whereas it does not if == is evaluated first. To
>>> enable an automatic check for such programs, we disallow all programs
>>> <P> where the execution of gcc -c -std=c99 -Wsequence-point <P> shows a
>>> warning."
>>>
>>> Thoughts?
>>>
>>> Best regards,
>>>
>>>   Thomas
>>>
>>> Am 28.07.2015 um 14:32 schrieb Akihisa Yamada:
>>>> Dear Matthias,
>>>>
>>>> I agree that it is hard to state precisely. On the other hand, gcc has
>>>> "-Wsequence-point" option to detect this kind of issues. I checked:
>>>>
>>>> for f in */*.c
>>>> do gcc -c -std=c99 -Wsequence-point -Wno-int-to-pointer-cast
>>>> -Wno-implicit-function-declaration -o /dev/null $f
>>>> done
>>>>
>>>> and found only one warning related to this:
>>>>
>>>> SV-COMP_Termination_Category/joey_false-termination.c: In function ‘rec’:
>>>> SV-COMP_Termination_Category/joey_false-termination.c:15:18: warning:
>>>> operation on ‘x’ may be undefined [-Wsequence-point]
>>>>
>>>>        return rec(++x) + rec(--x);
>>>>        
>>>>                   ^
>>>>
>>>> Best regards,
>>>> Akihisa
> 
> 
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 

-- 
Thomas Ströder        mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/stroeder
RWTH Aachen           phone: +49 241 80-21241
-------------- next part --------------
A non-text attachment was scrubbed...
Name: joey_false-termination.c
Type: text/x-csrc
Size: 428 bytes
Desc: not available
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150729/3e6727e7/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150729/3e6727e7/attachment.sig>