CBMC: Use instrumented malloc/free for MLD_ALLOC/MLD_FREE

The default implementation of MLD_ALLOC and MLD_FREE uses stack
allocation, which the compiler can assume not to fail. This means
that CBMC does not exercise the cleanup paths which handle fallible
dynamic allocation -- a significant proof gap.

This commit changes the configuration uses for the CBMC proofs
to use the (instrumented) calls to malloc/free for MLD_ALLOC/MLD_FREE.

Importantly, we set --malloc-may-fail to model allocation as fallible,
and --malloc-fail-null to return NULL in case of allocation failure.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

proofs/cbmc/Makefile.common

@@ -247,7 +247,7 @@ endif
 #   * an entire project when added to Makefile-project-defines
 #   * a specific proof when added to the harness Makefile
 
-CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-fail-assert
+CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail --malloc-fail-null # alloc may fail with returning NULL
 CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable
 CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
 CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable
@@ -555,6 +555,7 @@ ifndef MLD_CONFIG_PARAMETER_SET
     $(error MLD_CONFIG_PARAMETER_SET not set)
 endif
 
+DEFINES += -DMLD_CONFIG_FILE="\"mldsa_native_config_cbmc.h\""
 DEFINES += -DMLD_CONFIG_PARAMETER_SET=$(MLD_CONFIG_PARAMETER_SET)
 # Give visibility to all static functions
 DEFINES += -Dstatic=