Suppress spurious proof warning for gen_matrix()

gen_matrix() does not have loop invariants, so goto-instrument
warns about this, even though gen_matrix() is not called directly
by indcpa_enc() but it _does_ appears in the same translation unit.

The warning can be suppressed by explicitly adding gen_matrix()
to the USE_FUNCTION_CONTRACTS list in the Makefile.

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

proofs/cbmc/indcpa_enc/Makefile

@@ -23,6 +23,11 @@ CHECK_FUNCTION_CONTRACTS=mlk_indcpa_enc
 USE_FUNCTION_CONTRACTS = mlk_indcpa_enc_u
 USE_FUNCTION_CONTRACTS += mlk_indcpa_enc_v
 USE_FUNCTION_CONTRACTS += mlk_zeroize
+
+# Suppress spurious warning for gen_matrix() not having loop contracts
+# by making it appear to be call-by-contract
+USE_FUNCTION_CONTRACTS += mlk_gen_matrix
+
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1