[Termtools] About memory examples in C category

[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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part.
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150729/8756dd47/attachment.sig>