There are various fixes but the right thing here is to correctly put an array type (rather than a pointer type) in the signature. Of course, because miTLS, this cannot be made a strict thing and an unsound option exists to disable it. (miTLS does not rely on --cmi, which causes all sorts of problems).
This requires a corresponding fix on miTLS which I'll merge shortly; I have a local green on my machine.
This is an old issue but that was made much more difficult to deal with due to https://github.com/hacl-star/hacl-star/pull/897
There are various fixes but the right thing here is to correctly put an array type (rather than a pointer type) in the signature. Of course, because miTLS, this cannot be made a strict thing and an unsound option exists to disable it. (miTLS does not rely on --cmi, which causes all sorts of problems).
This requires a corresponding fix on miTLS which I'll merge shortly; I have a local green on my machine.