[Termtools] About memory examples in C category

[Thomas Ströder]

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
> 
> On 2015/07/28 5:00, Matthias Heizmann wrote:
>> Hi Thomas, hi all,
>>
>> On Monday, July 27, 2015 13:29:34 Thomas Ströder wrote:
>>> "Programs where the evaluation order of operations is not defined
>>> according to the C standard 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."
>>
>> I like the idea of "a rule like this". However, yet I do not have an
>> idea how
>> we can state such a rule precisely.
>>
>> I see two problems with your suggestion.
>> 1. What exactly is an operation? The C standard uses the term
>> "operation" but
>> I think it is never defined.
>>
>> 2. According to my notion of 'operation' your rule also forbids
>> programs that
>> contain the expression
>>      f1() + f2()
>> because the C standard does not define whether 'f1()' or 'f2()' is
>> evaluated
>> first. Is that you intension?
>> If yes, this is fine for me, but I guess then we have several programs
>> (at
>> least MutualRecursion_1a_false-termination.c) that have to be excluded
>> from
>> the competition.
>>
>> Furthermore, I think it is a problem that we do not have a tool that
>> can check
>> compliance with your rule. We would have to check all programs manually.
>>
>> Best,
>> Matthias
>>
>>
>> PS: Sorry for the delayed response. In the next days I will be able to
>> respond
>> more quickly.
>>
>>
>>
>>
>>
>>
>>
>> On Monday, July 27, 2015 13:29:34 Thomas Ströder wrote:
>>> Dear Akihisa,
>>>
>>> I agree with you. What about the following additional rule:
>>>
>>> "Programs where the evaluation order of operations is not defined
>>> according to the C standard 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."
>>>
>>> Would all participants of the C category be fine with that rule or do
>>> you see problems with it? If all participants agree, I would add it to
>>> the rules on termination-portal.
>>>
>>> Best regards,
>>>
>>>    Thomas
>>>
>>>
>>> _______________________________________________
>>> 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: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150728/c762d590/attachment.sig>