chore: update s2n_stuffer_printf CBMC harness (aws#4531)

tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c

@@ -21,6 +21,18 @@
 #include "stuffer/s2n_stuffer.h"
 #include "utils/s2n_mem.h"
 
+int nondet_int(void);
+
+int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
+{
+    if (size > 0)
+        __CPROVER_havoc_slice(str, size);
+    (void) *fmt;
+    if (__CPROVER_OBJECT_SIZE(ap) > 0)
+        (void) *(char **) ap;
+    return nondet_int();
+}
+
 void s2n_stuffer_printf_harness()
 {
     nondet_s2n_mem_init();
@@ -33,11 +45,12 @@ void s2n_stuffer_printf_harness()
 
     /* CBMC defines va_list as void** */
     size_t va_list_size;
-    __CPROVER_assume(va_list_size % sizeof(void*) == 0);
-    void** va_list_mem = malloc(va_list_size);
+    __CPROVER_assume(va_list_size % sizeof(void *) == 0);
+    void **va_list_mem = malloc(va_list_size);
+    __CPROVER_assume(va_list_mem != NULL);
 
     /* Store the stuffer to compare after the write */
-    struct s2n_stuffer            old_stuffer = *stuffer;
+    struct s2n_stuffer old_stuffer = *stuffer;
     struct store_byte_from_buffer old_byte;
     save_byte_from_array(old_stuffer.blob.data, old_stuffer.write_cursor, &old_byte);