bin/test.sh -c dev fails for this example.
GCC complains that a.out.frama.c:277:13: error: ‘__gen_e_acsl_v_2’ undeclared

The translation doesn't take into account the scenario that the same
logic function needs to be translated twice. This is due to different
call sites requiring different signatures.

The authors of the translation must worked with the assumption that
uniqueness of logic variables is a strong enough guarantee to be able to
reuse the translation of a logic variable can always be re-used.

This is wrong, since the translation of a logic variable can be re-used
within the context of one function translation, but escapes its scope if
it is re-used in another translation of the same function.