Undefined behavior in task `eureka_01-1.yml`

[MartinSpiessl]

Link to the current version of the program:
c/loops/eureka_01-1.c@d44f38aa

The tasks accesses uninitialized parts of the array int distance[5], which is in the scope of the function main (if it were in the global scope, accesses would be fine).
If we choose nodecount=1 and edgecount=1, only distance[0] gets written to in the first for-loop.
But then in the second loop (the nested one), since Dest[0] is 1 this means that distance[x] accesses distance[1], which is uninitialized.

Can someone confirm my reasoning that there is undefined behavior? Maybe there is a subtlety I overlooked, that would not be the first time. The reasoning would be via the C standard analogous to #817 (comment) and the following comment.

For fixing this, distance should probably always be initialized completely in the first loop, so the loop bound should always go up to 5. Then, however, there is no violation anymore, so in order to preserve the original violation the previously unintialized elements of distance should probably be initialized non-deterministically.

This task is also bit weird if you try to understand what is happening. The inner loop of the nested loop does never use the counter of the outside loop and is also not self-assigning like in eureka_01-2.c, so what is the effect/purpose of the outer loop? I would really like to get some insight from the original author about the intention behind this task (who is that, @dbeyer do you know? The README says the tasks are contributed by ESBMC, so @mikhailramalho or @feliperodri might know this as well.).

I find it remarkable that such an undefined behavior can hide in the benchmarks for 7 years. We are really missing a general property for (un)defined behavior. Otherwise we will not find those issues easily, and tasks get fixed without preserving the original task as an occurrence of undefined behavior.