From 6c40dee2f3150fd0a6b992403533276a00479b2b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 13 Jun 2024 10:45:35 +0200 Subject: [PATCH] chore: update s2n_stuffer_printf CBMC harness (#4531) --- .../s2n_stuffer_printf_harness.c | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c b/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c index e5fb8f593fe..e1b5dbbd162 100644 --- a/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c +++ b/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);