Implementation-defined behaviour
hernanponcedeleon opened this issue · 3 comments
How are we supposed to interpret "implementation-defined behaviour"?
My understanding is that this is "danger zone" and we should avoid them if possible. However I found this benchmark by @Heizmann which exercise exactly this and it is marked as no-overflow, suggesting SVCOMP does not consider implementation-defined behaviour "dangerous" (or to be avoided as undefined behaviour).
To give some context, the reducercommutativity/rangesum(X).c
benchmarks fit in this pattern.
int rangesum (int x[N])
{
...
long long ret;
...
if ( cnt !=0)
return ret / cnt;
else
return 0;
}
int main ()
{
...
int ret;
....
ret = fun(x);
...
}
The initial version of the benchmarks defined ret
(in rangesum
) as an int
. Later it was changed to long long
due to a possible overflow (not shown here). I think the best for this kind of benchmarks would be to change the return value of rangesum
and the value of ret
in main
to long long
.
How are we supposed to interpret "implementation-defined behaviour"?
The programs in this repository are to be interpreted as GNU C, so where the standard mentions implementation-defined behavior we need to check what gcc defines.
Can this be closed or are there open questions?
Yes.