Fix CBMC

aws · Feb 28, 2023 · f05489d · f05489d
1 parent 9ca4434
commit f05489d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git a/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile b/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile
@@ -44,6 +44,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 
 # We abstract this function because manual inspection demonstrates it is unreachable.
+REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 REMOVE_FUNCTION_BODY += s2n_stuffer_resize
 REMOVE_FUNCTION_BODY += s2n_stuffer_rewrite
 REMOVE_FUNCTION_BODY += s2n_add_overflow

diff --git a/...s/cbmc/proofs/s2n_stuffer_private_key_from_pem/s2n_stuffer_private_key_from_pem_harness.c b/...s/cbmc/proofs/s2n_stuffer_private_key_from_pem/s2n_stuffer_private_key_from_pem_harness.c
@@ -16,16 +16,14 @@
 #include <assert.h>
 #include <cbmc_proof/cbmc_utils.h>
 #include <cbmc_proof/make_common_datastructures.h>
-#include <string.h>
 
 #include "api/s2n.h"
-#include "stuffer/s2n_stuffer.h"
-#include "utils/s2n_mem.h"
 
 void s2n_stuffer_private_key_from_pem_harness()
 {
     /* Non-deterministic inputs. */
     struct s2n_stuffer *pem = cbmc_allocate_s2n_stuffer();
+    int *type = malloc(sizeof(int));
     __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(pem)));
     __CPROVER_assume(s2n_blob_is_bounded(&pem->blob, MAX_BLOB_SIZE));
 
@@ -35,7 +33,7 @@ void s2n_stuffer_private_key_from_pem_harness()
     nondet_s2n_mem_init();
 
     /* Operation under verification. */
-    s2n_stuffer_private_key_from_pem(pem, asn1);
+    s2n_stuffer_private_key_from_pem(pem, asn1, type);
 
     /* Post-conditions. */
     assert(s2n_result_is_ok(s2n_stuffer_validate(pem)));