FStarLang/karamel

Improper C generation with update_sub and NULL

sonmarcho opened this issue · 0 comments

When extracting the following Low*:

let f () : Stack unit (fun _ -> True) (fun _ _ _ -> True) =
  blit #bool null 0ul null 0ul 0ul

We get the following C code:

void Kremlin1_f()
{
  memcpy(NULL, NULL, (uint32_t)0U * sizeof (NULL[0U]));
}

This doesn't compile since NULL[0U] is not legal