Benjamin Beurdouche

I think having documentation in the C code (working on that) should be the answer because the user should be using it properly anyway, but fair enough, let us think...

The code is voluntarily not defensive, there is a precondition that is that you should not be passing a null pointer to that function. I think this should be better...

https://hacl-star.github.io/HaclAEAD.html

Note, that because passing a null aad is quite frequent, I protected the call in #413 so that if the length is zero you won't have to pass a non-null...

?? Maybe it is working, but I have no knowledge of HACL* being compiled with MSVC at the moment.

Ok, I'll look into restoring it then. Thanks Jonathan !

@protz is MSVC covered by the CI these days ?

`gcc 4.8` it is. Maybe someone has stronger requirements @polubelova @Frosne @protz ?

I think @Frosne is running into exactly that right now in our CI.

> @Kachoc and I have discussed this repeatedly and have come to the conclusion that there should be one test file per vectorization level (just like there is one C...