Perform null-checks when assigning initial value of heap allocations

[msprotz]

Previously, we operated in a model where the amount of heap memory was infinite.

For the first time (to the best of my knowledge), a piece of code started leveraging the "partial" allocation functions in the Low* libraries, here: hacl-star/hacl-star#1007. Partial allocation functions (also known as fallible) may return NULL, and the user must check that the result is non-null before doing anything with it.

This NULL-check was defeated by the fact that the initial value for the heap allocation (as provided in the Low* model) had to be compiled to an assignment (in C) that operates after the malloc but before the user got a chance to check for NULL...

The fix is simply to always guard such assignments (for the initial value to be stored in the heap allocation) to be behind null-checks.

• Either the user was usable the fallible malloc, in which a null-check is forthcoming -- great, or
• the user was using the infallible malloc, meaning that all bets were off anyhow in case of allocation failure, we just defer the failure to a potential later point.

CC @tahina-pro