[Termtools] About memory examples in C category

[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

-- 
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: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150729/174ee2d9/attachment.sig>