Improper C generation with update_sub and NULL
sonmarcho opened this issue · 0 comments
sonmarcho commented
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