Remove unneeded assumptions and use nondet values

Replace precondition by false case in enc_request validator

source/default_cmm.c

@@ -187,7 +187,8 @@ int aws_cryptosdk_default_cmm_set_alg_id(struct aws_cryptosdk_cmm *cmm, enum aws
 }
 
 bool aws_cryptosdk_default_cmm_is_valid(const struct aws_cryptosdk_cmm *cmm) {
-    AWS_PRECONDITION(cmm != NULL);
+    if (cmm == NULL) return false;
+
     struct default_cmm *self = (struct default_cmm *)cmm;
     return aws_cryptosdk_cmm_base_is_valid(&self->base) && aws_allocator_is_valid(self->alloc) &&
            aws_cryptosdk_keyring_is_valid(self->kr);

verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

@@ -41,14 +41,10 @@ void default_cmm_generate_enc_materials_harness() {
     struct aws_cryptosdk_enc_request *request  = ensure_enc_request_attempt_allocation(MAX_TABLE_SIZE);
 
     /* Assumptions */
-    __CPROVER_assume(cmm != NULL);
     __CPROVER_assume(aws_cryptosdk_default_cmm_is_valid(cmm));
 
     __CPROVER_assume(output != NULL);
 
-    __CPROVER_assume(request != NULL);
-    __CPROVER_assume(aws_allocator_is_valid(request->alloc));
-    __CPROVER_assume(request->enc_ctx != NULL);
     __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request));
 
     /* Save current state of the data structures */

verification/cbmc/sources/make_common_data_structures.c

@@ -422,7 +422,7 @@ struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(const struct aws
     struct default_cmm *self = NULL;
     if (cmm) {
         self        = (struct default_cmm *)cmm;
-        self->alloc = can_fail_allocator();
+        self->alloc = nondet_bool()? NULL : can_fail_allocator();
         self->kr    = keyring;
     }
     return (struct aws_cryptosdk_cmm *)self;

verification/cbmc/stubs/on_encrypt_stub.c

@@ -69,6 +69,5 @@ int on_encrypt(
          */
         if (nondet_bool()) ensure_byte_buf_has_allocated_buffer_member(unencrypted_data_key);
     }
-    int ret;
-    return ret;
+    return nondet_int();
 }