https://gcc.gnu.org/bugzilla/show_bug.cgi?id=88531
--- Comment #13 from H.J. Lu <hjl.tools at gmail dot com> --- Here is the equivalent C code: --- #include <stdint.h> #define loop_t uint32_t #define idx_t uint32_t void loop(double * const __restrict__ dst, double const * const __restrict__ src, idx_t const * const __restrict__ idx, loop_t const begin, loop_t const end) { for (loop_t i = begin; i < end; ++i) dst[i] = 42.0 * src[idx[i]]; } ---