Implementation-defined behaviour

[hernanponcedeleon]

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.

[PhilippWendler]

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.

[PhilippWendler]

Can this be closed or are there open questions?

[hernanponcedeleon]

Yes.