CBMC version: 5.12 (cbmc-5.12.1-10-gdf2638c59)
Operating system: macOS Mojave Version 10.14.6
Exact command line resulting in the issue: Run s2n_array_new proof.
What behaviour did you expect: Verification Successful.
What happened instead: Invariant check failed.
To reproduce the error, clone cbmc-array-set-predicates branch and go to s2n/tests/cbmc/proofs/s2n_array_new dir. To run the proof harness, just enter make cbmc (you need goto-cc, goto-instrument, goto-analyzer, and cbmc on your $PATH). I got the following error message:
Very long log
```
~/Development/s2n/tests/cbmc/proofs/s2n_array_new
$ make cbmc
goto-instrument --verbosity 4 --remove-function-body s2n_blob_slice --remove-function-body s2n_ensure_memcpy_trace --remove-function-body abort /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness0.goto /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness1.goto 2>&1 | tee /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/logs/s2n_array_new_harness1.log; exit ${PIPESTATUS[0]}
No function abort in goto program
goto-cc --verbosity 4 --function s2n_array_new_harness /home/tspriggs/Development/s2n/tests/cbmc/stubs/memset.c /home/tspriggs/Development/s2n/tests/cbmc/stubs/abort_override_assert_false.c -I/home/tspriggs/Development/s2n/tests/cbmc/include/ -I/home/tspriggs/Development/s2n -I/home/tspriggs/Development/s2n/api -DCBMC_OBJECT_BITS=8 -DCBMC=1 -DAWS_DEEP_CHECKS=0 /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness1.goto -o /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness2.goto 2>&1 | tee /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/logs/s2n_array_new_harness2.log; exit ${PIPESTATUS[0]}
cp /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness2.goto /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness3.goto; echo "Not unwinding goto program" | tee /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/logs/s2n_array_new_harness3.log
Not unwinding goto program
cp /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness3.goto /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness4.goto; echo "Not generating-function-bodies in goto program" | tee /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/logs/s2n_array_new_harness4.log
Not generating-function-bodies in goto program
cp /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness4.goto /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness5.goto; echo "Not simplfying goto program" | tee /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/logs/s2n_array_new_harness5.log
Not simplfying goto program
goto-instrument --verbosity 4 --drop-unused-functions /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness5.goto /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness6.goto 2>&1 | tee /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/logs/s2n_array_new_harness6.log; exit ${PIPESTATUS[0]}
goto-instrument --verbosity 4 --slice-global-inits /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness6.goto /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness7.goto 2>&1 | tee /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/logs/s2n_array_new_harness7.log; exit ${PIPESTATUS[0]}
cp /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness7.goto /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness.goto
cbmc --verbosity 4 --unwind 1 --object-bits 8 --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --trace /home/tspriggs/Development/s2n/tests/cbmc/proofs/s2n_array_new/gotos/s2n_array_new_harness.goto 2>&1 | tee logs/cbmc.log; if [ ${PIPESTATUS[0]} -ne 10 ]; then exit ${PIPESTATUS[0]}; fi
**** WARNING: no body for function sysconf
**** WARNING: no body for function s2n_calculate_stacktrace
**** WARNING: no body for function madvise
**** WARNING: no body for function mlock
**** WARNING: no body for function munlock
**** WARNING: no body for function s2n_blob_slice
**** WARNING: no body for function s2n_ensure_memcpy_trace
** Results:
/home/tspriggs/Development/s2n/tests/cbmc/stubs/memset.c function memset
[memset.overflow.1] line 47 arithmetic overflow on signed to unsigned type conversion in (size_t)POINTER_OFFSET(s): SUCCESS
[memset.overflow.2] line 47 arithmetic overflow on unsigned + in (size_t)POINTER_OFFSET(s) + n: SUCCESS
[memset.overflow.3] line 47 arithmetic overflow on signed to unsigned type conversion in (size_t)POINTER_OFFSET(s): SUCCESS
[memset.overflow.4] line 47 arithmetic overflow on unsigned + in (size_t)POINTER_OFFSET(s) + n: SUCCESS
[memset.precondition_instance.1] line 47 memset destination region writeable: SUCCESS
/home/tspriggs/Development/s2n/tests/cbmc/stubs/memset.c function memset_impl
[memset_impl.overflow.1] line 41 arithmetic overflow on unsigned to signed type conversion in (signed long int)index: SUCCESS
[memset_impl.overflow.2] line 41 pointer arithmetic overflow on + in (uint8_t *)s + (signed long int)index: SUCCESS
[memset_impl.pointer_dereference.1] line 41 dereference failure: pointer invalid in ((uint8_t *)s)[(signed long int)index]: SUCCESS
[memset_impl.pointer_dereference.2] line 41 dereference failure: pointer NULL in ((uint8_t *)s)[(signed long int)index]: SUCCESS
[memset_impl.pointer_dereference.3] line 41 dereference failure: deallocated dynamic object in ((uint8_t *)s)[(signed long int)index]: SUCCESS
[memset_impl.pointer_dereference.4] line 41 dereference failure: dead object in ((uint8_t *)s)[(signed long int)index]: SUCCESS
[memset_impl.pointer_dereference.5] line 41 dereference failure: pointer outside dynamic object bounds in ((uint8_t *)s)[(signed long int)index]: SUCCESS
[memset_impl.pointer_dereference.6] line 41 dereference failure: pointer outside object bounds in ((uint8_t *)s)[(signed long int)index]: SUCCESS
[memset_impl.pointer_dereference.7] line 41 dereference failure: invalid integer address in ((uint8_t *)s)[(signed long int)index]: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_array.c function s2n_array_enlarge
[s2n_array_enlarge.overflow.1] line 30 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)array): SUCCESS
[s2n_array_enlarge.overflow.2] line 30 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)array) + sizeof(struct s2n_array) /*32ul*/ : SUCCESS
[s2n_array_enlarge.overflow.3] line 30 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)array): SUCCESS
[s2n_array_enlarge.overflow.4] line 30 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)array) + sizeof(struct s2n_array) /*32ul*/ : SUCCESS
[s2n_array_enlarge.pointer_dereference.1] line 34 dereference failure: pointer invalid in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.2] line 34 dereference failure: pointer NULL in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.3] line 34 dereference failure: deallocated dynamic object in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.4] line 34 dereference failure: dead object in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.5] line 34 dereference failure: pointer outside dynamic object bounds in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.6] line 34 dereference failure: pointer outside object bounds in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.7] line 34 dereference failure: invalid integer address in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.8] line 39 dereference failure: pointer invalid in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.9] line 39 dereference failure: pointer NULL in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.10] line 39 dereference failure: deallocated dynamic object in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.11] line 39 dereference failure: dead object in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.12] line 39 dereference failure: pointer outside dynamic object bounds in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.13] line 39 dereference failure: pointer outside object bounds in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.14] line 39 dereference failure: invalid integer address in array->element_size: SUCCESS
[s2n_array_enlarge.pointer_dereference.15] line 39 dereference failure: pointer outside dynamic object bounds in array->len: SUCCESS
[s2n_array_enlarge.pointer_dereference.16] line 39 dereference failure: pointer outside object bounds in array->len: SUCCESS
[s2n_array_enlarge.pointer_dereference.17] line 39 dereference failure: invalid integer address in array->len: SUCCESS
[s2n_array_enlarge.overflow.5] line 40 arithmetic overflow on unsigned - in array->mem.size - array_elements_size: SUCCESS
[s2n_array_enlarge.overflow.6] line 40 pointer arithmetic overflow on + in array->mem.data + (signed long int)array_elements_size: SUCCESS
[s2n_array_enlarge.overflow.7] line 40 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)__tmp_d): SUCCESS
[s2n_array_enlarge.overflow.8] line 40 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)__tmp_d) + sizeof(uint8_t) /*1ul*/ : SUCCESS
[s2n_array_enlarge.overflow.9] line 40 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)__tmp_d): SUCCESS
[s2n_array_enlarge.overflow.10] line 40 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)__tmp_d) + sizeof(uint8_t) /*1ul*/ : SUCCESS
[s2n_array_enlarge.pointer_dereference.18] line 40 dereference failure: pointer invalid in array->mem: SUCCESS
[s2n_array_enlarge.pointer_dereference.19] line 40 dereference failure: pointer NULL in array->mem: SUCCESS
[s2n_array_enlarge.pointer_dereference.20] line 40 dereference failure: deallocated dynamic object in array->mem: SUCCESS
[s2n_array_enlarge.pointer_dereference.21] line 40 dereference failure: dead object in array->mem: SUCCESS
[s2n_array_enlarge.pointer_dereference.22] line 40 dereference failure: pointer outside dynamic object bounds in array->mem: SUCCESS
[s2n_array_enlarge.pointer_dereference.23] line 40 dereference failure: pointer outside object bounds in array->mem: SUCCESS
[s2n_array_enlarge.pointer_dereference.24] line 40 dereference failure: invalid integer address in array->mem: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_array.c function s2n_array_is_valid
[s2n_array_is_valid.overflow.1] line 24 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)array): SUCCESS
[s2n_array_is_valid.overflow.2] line 24 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)array) + sizeof(const struct s2n_array) /*32ul*/ : SUCCESS
[s2n_array_is_valid.overflow.3] line 24 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)array): SUCCESS
[s2n_array_is_valid.overflow.4] line 24 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)array) + sizeof(const struct s2n_array) /*32ul*/ : SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_array.c function s2n_array_new
[s2n_array_new.pointer_dereference.1] line 52 dereference failure: pointer invalid in *array: SUCCESS
[s2n_array_new.pointer_dereference.2] line 52 dereference failure: pointer NULL in *array: SUCCESS
[s2n_array_new.pointer_dereference.3] line 52 dereference failure: deallocated dynamic object in *array: SUCCESS
[s2n_array_new.pointer_dereference.4] line 52 dereference failure: dead object in *array: SUCCESS
[s2n_array_new.pointer_dereference.5] line 52 dereference failure: pointer outside dynamic object bounds in *array: SUCCESS
[s2n_array_new.pointer_dereference.6] line 52 dereference failure: pointer outside object bounds in *array: SUCCESS
[s2n_array_new.pointer_dereference.7] line 52 dereference failure: invalid integer address in *array: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_blob.c function s2n_blob_is_valid
[s2n_blob_is_valid.overflow.1] line 29 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)b): SUCCESS
[s2n_blob_is_valid.overflow.2] line 29 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)b) + sizeof(const struct s2n_blob) /*24ul*/ : SUCCESS
[s2n_blob_is_valid.overflow.3] line 29 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)b): SUCCESS
[s2n_blob_is_valid.overflow.4] line 29 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)b) + sizeof(const struct s2n_blob) /*24ul*/ : SUCCESS
[s2n_blob_is_valid.pointer_dereference.1] line 30 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.2] line 30 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.3] line 30 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.4] line 30 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.5] line 30 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.6] line 30 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.7] line 30 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.8] line 30 dereference failure: pointer invalid in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.9] line 30 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.10] line 30 dereference failure: deallocated dynamic object in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.11] line 30 dereference failure: dead object in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.12] line 30 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.13] line 30 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.14] line 30 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.15] line 31 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.16] line 31 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.17] line 31 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.18] line 31 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.19] line 31 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.20] line 31 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.21] line 31 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.22] line 31 dereference failure: pointer invalid in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.23] line 31 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.24] line 31 dereference failure: deallocated dynamic object in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.25] line 31 dereference failure: dead object in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.26] line 31 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.27] line 31 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.28] line 31 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.29] line 32 dereference failure: pointer invalid in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.30] line 32 dereference failure: pointer NULL in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.31] line 32 dereference failure: deallocated dynamic object in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.32] line 32 dereference failure: dead object in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.33] line 32 dereference failure: pointer outside dynamic object bounds in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.34] line 32 dereference failure: pointer outside object bounds in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.35] line 32 dereference failure: invalid integer address in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.36] line 32 dereference failure: pointer invalid in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.37] line 32 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.38] line 32 dereference failure: deallocated dynamic object in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.39] line 32 dereference failure: dead object in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.40] line 32 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.41] line 32 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.42] line 32 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.43] line 33 dereference failure: pointer invalid in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.44] line 33 dereference failure: pointer NULL in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.45] line 33 dereference failure: deallocated dynamic object in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.46] line 33 dereference failure: dead object in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.47] line 33 dereference failure: pointer outside dynamic object bounds in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.48] line 33 dereference failure: pointer outside object bounds in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.49] line 33 dereference failure: invalid integer address in b->growable: SUCCESS
[s2n_blob_is_valid.pointer_dereference.50] line 33 dereference failure: pointer invalid in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.51] line 33 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.52] line 33 dereference failure: deallocated dynamic object in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.53] line 33 dereference failure: dead object in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.54] line 33 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.55] line 33 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.56] line 33 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.57] line 33 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.58] line 33 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.59] line 33 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_blob_is_valid.overflow.5] line 34 arithmetic overflow on signed to unsigned type conversion in (__CPROVER_size_t)POINTER_OFFSET((const void *)b->data): SUCCESS
[s2n_blob_is_valid.overflow.6] line 34 arithmetic overflow on unsigned + in (__CPROVER_size_t)POINTER_OFFSET((const void *)b->data) + (__CPROVER_size_t)b->allocated: SUCCESS
[s2n_blob_is_valid.overflow.7] line 34 arithmetic overflow on signed to unsigned type conversion in (__CPROVER_size_t)POINTER_OFFSET((const void *)b->data): SUCCESS
[s2n_blob_is_valid.overflow.8] line 34 arithmetic overflow on unsigned + in (__CPROVER_size_t)POINTER_OFFSET((const void *)b->data) + (__CPROVER_size_t)b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.60] line 34 dereference failure: pointer invalid in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.61] line 34 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.62] line 34 dereference failure: deallocated dynamic object in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.63] line 34 dereference failure: dead object in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.64] line 34 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.65] line 34 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.66] line 34 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.67] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.68] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.69] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.70] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.71] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.72] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.73] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.74] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.75] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.76] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.77] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.78] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.79] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.80] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.81] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.82] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.83] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.84] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.85] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.86] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.87] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.88] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.89] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.90] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.91] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.92] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.93] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.94] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.95] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.96] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.97] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.98] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.99] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.100] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.101] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.102] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.103] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.104] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.105] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.106] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.107] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.108] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.109] line 34 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.110] line 34 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.111] line 34 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.112] line 34 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.113] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.114] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.115] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.116] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.117] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.118] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.119] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.120] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.121] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.122] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.123] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.124] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.125] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.126] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.127] line 34 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.128] line 34 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.129] line 34 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.130] line 34 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_blob_is_valid.pointer_dereference.131] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.132] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.133] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.134] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.135] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.136] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.137] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.138] line 34 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.139] line 34 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.140] line 34 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.141] line 34 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.142] line 34 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.143] line 34 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.144] line 34 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.overflow.9] line 35 arithmetic overflow on signed to unsigned type conversion in (__CPROVER_size_t)POINTER_OFFSET((const void *)b->data): SUCCESS
[s2n_blob_is_valid.overflow.10] line 35 arithmetic overflow on unsigned + in (__CPROVER_size_t)POINTER_OFFSET((const void *)b->data) + (__CPROVER_size_t)b->size: SUCCESS
[s2n_blob_is_valid.overflow.11] line 35 arithmetic overflow on signed to unsigned type conversion in (__CPROVER_size_t)POINTER_OFFSET((const void *)b->data): SUCCESS
[s2n_blob_is_valid.overflow.12] line 35 arithmetic overflow on unsigned + in (__CPROVER_size_t)POINTER_OFFSET((const void *)b->data) + (__CPROVER_size_t)b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.145] line 35 dereference failure: pointer invalid in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.146] line 35 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.147] line 35 dereference failure: deallocated dynamic object in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.148] line 35 dereference failure: dead object in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.149] line 35 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.150] line 35 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.151] line 35 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.152] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.153] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.154] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.155] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.156] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.157] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.158] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.159] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.160] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.161] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.162] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.163] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.164] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.165] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.166] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.167] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.168] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.169] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.170] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.171] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.172] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.173] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.174] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.175] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.176] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.177] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.178] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.179] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.180] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.181] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.182] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.183] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.184] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.185] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.186] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.187] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.188] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.189] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.190] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.191] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.192] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.193] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.194] line 35 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.195] line 35 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.196] line 35 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.197] line 35 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.198] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.199] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.200] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.201] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.202] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.203] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.204] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.205] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.206] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.207] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.208] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.209] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.210] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.211] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.212] line 35 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.213] line 35 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.214] line 35 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.215] line 35 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_blob_is_valid.pointer_dereference.216] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.217] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.218] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.219] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.220] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.221] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.222] line 35 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.223] line 35 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.224] line 35 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.225] line 35 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.226] line 35 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.227] line 35 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.228] line 35 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_valid.pointer_dereference.229] line 35 dereference failure: invalid integer address in b->data: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_blob.c function s2n_blob_zero
[s2n_blob_zero.overflow.1] line 50 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)__tmp_d): SUCCESS
[s2n_blob_zero.overflow.2] line 50 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)__tmp_d) + sizeof(uint8_t) /*1ul*/ : SUCCESS
[s2n_blob_zero.overflow.3] line 50 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)__tmp_d): SUCCESS
[s2n_blob_zero.overflow.4] line 50 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)__tmp_d) + sizeof(uint8_t) /*1ul*/ : SUCCESS
[s2n_blob_zero.pointer_dereference.1] line 50 dereference failure: pointer invalid in b->allocated: SUCCESS
[s2n_blob_zero.pointer_dereference.2] line 50 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_blob_zero.pointer_dereference.3] line 50 dereference failure: deallocated dynamic object in b->allocated: SUCCESS
[s2n_blob_zero.pointer_dereference.4] line 50 dereference failure: dead object in b->allocated: SUCCESS
[s2n_blob_zero.pointer_dereference.5] line 50 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_blob_zero.pointer_dereference.6] line 50 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_blob_zero.pointer_dereference.7] line 50 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_blob_zero.pointer_dereference.8] line 50 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.9] line 50 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.10] line 50 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.11] line 50 dereference failure: pointer invalid in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.12] line 50 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.13] line 50 dereference failure: deallocated dynamic object in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.14] line 50 dereference failure: dead object in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.15] line 50 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.16] line 50 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.17] line 50 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_blob_zero.pointer_dereference.18] line 50 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_zero.pointer_dereference.19] line 50 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_zero.pointer_dereference.20] line 50 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_zero.pointer_dereference.21] line 50 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_zero.pointer_dereference.22] line 50 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_zero.pointer_dereference.23] line 50 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_zero.pointer_dereference.24] line 50 dereference failure: invalid integer address in b->data: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_alloc
[s2n_alloc.overflow.1] line 150 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)b): SUCCESS
[s2n_alloc.overflow.2] line 150 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)b) + sizeof(struct s2n_blob) /*24ul*/ : SUCCESS
[s2n_alloc.overflow.3] line 150 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)b): SUCCESS
[s2n_alloc.overflow.4] line 150 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)b) + sizeof(struct s2n_blob) /*24ul*/ : SUCCESS
[s2n_alloc.pointer_dereference.1] line 152 dereference failure: pointer invalid in *b: SUCCESS
[s2n_alloc.pointer_dereference.2] line 152 dereference failure: pointer NULL in *b: SUCCESS
[s2n_alloc.pointer_dereference.3] line 152 dereference failure: deallocated dynamic object in *b: SUCCESS
[s2n_alloc.pointer_dereference.4] line 152 dereference failure: dead object in *b: SUCCESS
[s2n_alloc.pointer_dereference.5] line 152 dereference failure: pointer outside dynamic object bounds in *b: SUCCESS
[s2n_alloc.pointer_dereference.6] line 152 dereference failure: pointer outside object bounds in *b: SUCCESS
[s2n_alloc.pointer_dereference.7] line 152 dereference failure: invalid integer address in *b: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_blob_is_growable
[s2n_blob_is_growable.pointer_dereference.1] line 160 dereference failure: pointer invalid in b->growable: SUCCESS
[s2n_blob_is_growable.pointer_dereference.2] line 160 dereference failure: pointer NULL in b->growable: SUCCESS
[s2n_blob_is_growable.pointer_dereference.3] line 160 dereference failure: deallocated dynamic object in b->growable: SUCCESS
[s2n_blob_is_growable.pointer_dereference.4] line 160 dereference failure: dead object in b->growable: SUCCESS
[s2n_blob_is_growable.pointer_dereference.5] line 160 dereference failure: pointer outside dynamic object bounds in b->growable: SUCCESS
[s2n_blob_is_growable.pointer_dereference.6] line 160 dereference failure: pointer outside object bounds in b->growable: SUCCESS
[s2n_blob_is_growable.pointer_dereference.7] line 160 dereference failure: invalid integer address in b->growable: SUCCESS
[s2n_blob_is_growable.pointer_dereference.8] line 160 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_blob_is_growable.pointer_dereference.9] line 160 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_blob_is_growable.pointer_dereference.10] line 160 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_blob_is_growable.pointer_dereference.11] line 160 dereference failure: dead object in b->data: SUCCESS
[s2n_blob_is_growable.pointer_dereference.12] line 160 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_blob_is_growable.pointer_dereference.13] line 160 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_blob_is_growable.pointer_dereference.14] line 160 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_blob_is_growable.pointer_dereference.15] line 160 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_blob_is_growable.pointer_dereference.16] line 160 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_blob_is_growable.pointer_dereference.17] line 160 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_blob_is_growable.pointer_dereference.18] line 160 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_blob_is_growable.pointer_dereference.19] line 160 dereference failure: pointer invalid in b->allocated: SUCCESS
[s2n_blob_is_growable.pointer_dereference.20] line 160 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_blob_is_growable.pointer_dereference.21] line 160 dereference failure: deallocated dynamic object in b->allocated: SUCCESS
[s2n_blob_is_growable.pointer_dereference.22] line 160 dereference failure: dead object in b->allocated: SUCCESS
[s2n_blob_is_growable.pointer_dereference.23] line 160 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_blob_is_growable.pointer_dereference.24] line 160 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_blob_is_growable.pointer_dereference.25] line 160 dereference failure: invalid integer address in b->allocated: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_free
[s2n_free.pointer_dereference.1] line 269 dereference failure: pointer invalid in s2n_mem_free_cb: SUCCESS
[s2n_free.pointer_dereference.2] line 269 dereference failure: pointer NULL in s2n_mem_free_cb: SUCCESS
[s2n_free.pointer_dereference.3] line 269 dereference failure: deallocated dynamic object in s2n_mem_free_cb: SUCCESS
[s2n_free.pointer_dereference.4] line 269 dereference failure: dead object in s2n_mem_free_cb: SUCCESS
[s2n_free.pointer_dereference.5] line 269 dereference failure: pointer outside dynamic object bounds in s2n_mem_free_cb: SUCCESS
[s2n_free.pointer_dereference.6] line 269 dereference failure: pointer outside object bounds in s2n_mem_free_cb: SUCCESS
[s2n_free.pointer_dereference.7] line 269 dereference failure: invalid integer address in s2n_mem_free_cb: SUCCESS
[s2n_free.pointer_dereference.8] line 269 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_free.pointer_dereference.9] line 269 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_free.pointer_dereference.10] line 269 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_free.pointer_dereference.11] line 269 dereference failure: dead object in b->data: SUCCESS
[s2n_free.pointer_dereference.12] line 269 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_free.pointer_dereference.13] line 269 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_free.pointer_dereference.14] line 269 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_free.pointer_dereference.15] line 269 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_free.pointer_dereference.16] line 269 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_free.pointer_dereference.17] line 269 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_free.pointer_dereference.18] line 269 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_free.pointer_dereference.19] line 269 dereference failure: pointer invalid in b->data: SUCCESS
[s2n_free.pointer_dereference.20] line 269 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_free.pointer_dereference.21] line 269 dereference failure: deallocated dynamic object in b->data: SUCCESS
[s2n_free.pointer_dereference.22] line 269 dereference failure: dead object in b->data: SUCCESS
[s2n_free.pointer_dereference.23] line 269 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_free.pointer_dereference.24] line 269 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_free.pointer_dereference.25] line 269 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_free.pointer_dereference.26] line 269 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_free.pointer_dereference.27] line 269 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_free.pointer_dereference.28] line 269 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_free.pointer_dereference.29] line 269 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_free.pointer_dereference.30] line 271 dereference failure: pointer invalid in *b: SUCCESS
[s2n_free.pointer_dereference.31] line 271 dereference failure: pointer NULL in *b: SUCCESS
[s2n_free.pointer_dereference.32] line 271 dereference failure: deallocated dynamic object in *b: SUCCESS
[s2n_free.pointer_dereference.33] line 271 dereference failure: dead object in *b: SUCCESS
[s2n_free.pointer_dereference.34] line 271 dereference failure: pointer outside dynamic object bounds in *b: SUCCESS
[s2n_free.pointer_dereference.35] line 271 dereference failure: pointer outside object bounds in *b: SUCCESS
[s2n_free.pointer_dereference.36] line 271 dereference failure: invalid integer address in *b: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_mem_free_mlock_impl
[s2n_mem_free_mlock_impl.precondition_instance.1] line 72 free argument must be NULL or valid pointer: SUCCESS
[s2n_mem_free_mlock_impl.precondition_instance.2] line 72 free argument must be dynamic object: SUCCESS
[s2n_mem_free_mlock_impl.precondition_instance.3] line 72 free argument has offset zero: SUCCESS
[s2n_mem_free_mlock_impl.precondition_instance.4] line 72 double free: SUCCESS
[s2n_mem_free_mlock_impl.precondition_instance.5] line 72 free called for new[] object: SUCCESS
[s2n_mem_free_mlock_impl.precondition_instance.6] line 72 free called for stack-allocated object: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_mem_free_no_mlock_impl
[s2n_mem_free_no_mlock_impl.precondition_instance.1] line 80 free argument must be NULL or valid pointer: SUCCESS
[s2n_mem_free_no_mlock_impl.precondition_instance.2] line 80 free argument must be dynamic object: SUCCESS
[s2n_mem_free_no_mlock_impl.precondition_instance.3] line 80 free argument has offset zero: SUCCESS
[s2n_mem_free_no_mlock_impl.precondition_instance.4] line 80 double free: SUCCESS
[s2n_mem_free_no_mlock_impl.precondition_instance.5] line 80 free called for new[] object: SUCCESS
[s2n_mem_free_no_mlock_impl.precondition_instance.6] line 80 free called for stack-allocated object: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_mem_init
[s2n_mem_init.pointer_dereference.1] line 244 dereference failure: pointer invalid in s2n_mem_init_cb: SUCCESS
[s2n_mem_init.pointer_dereference.2] line 244 dereference failure: pointer NULL in s2n_mem_init_cb: SUCCESS
[s2n_mem_init.pointer_dereference.3] line 244 dereference failure: deallocated dynamic object in s2n_mem_init_cb: SUCCESS
[s2n_mem_init.pointer_dereference.4] line 244 dereference failure: dead object in s2n_mem_init_cb: SUCCESS
[s2n_mem_init.pointer_dereference.5] line 244 dereference failure: pointer outside dynamic object bounds in s2n_mem_init_cb: SUCCESS
[s2n_mem_init.pointer_dereference.6] line 244 dereference failure: pointer outside object bounds in s2n_mem_init_cb: SUCCESS
[s2n_mem_init.pointer_dereference.7] line 244 dereference failure: invalid integer address in s2n_mem_init_cb: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_mem_init_impl
[s2n_mem_init_impl.overflow.1] line 52 arithmetic overflow on signed to unsigned type conversion in (uint32_t)sysconf_rc: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_mem_malloc_mlock_impl
[s2n_mem_malloc_mlock_impl.overflow.1] line 87 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)ptr): SUCCESS
[s2n_mem_malloc_mlock_impl.overflow.2] line 87 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)ptr) + sizeof(void *) /*8ul*/ : SUCCESS
[s2n_mem_malloc_mlock_impl.overflow.3] line 87 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)ptr): SUCCESS
[s2n_mem_malloc_mlock_impl.overflow.4] line 87 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)ptr) + sizeof(void *) /*8ul*/ : SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.1] line 94 dereference failure: pointer invalid in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.2] line 94 dereference failure: pointer NULL in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.3] line 94 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.4] line 94 dereference failure: dead object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.5] line 94 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.6] line 94 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.7] line 94 dereference failure: invalid integer address in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.8] line 96 dereference failure: pointer invalid in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.9] line 96 dereference failure: pointer NULL in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.10] line 96 dereference failure: deallocated dynamic object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.11] line 96 dereference failure: dead object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.12] line 96 dereference failure: pointer outside dynamic object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.13] line 96 dereference failure: pointer outside object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.14] line 96 dereference failure: invalid integer address in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.15] line 103 dereference failure: pointer invalid in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.16] line 103 dereference failure: pointer NULL in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.17] line 103 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.18] line 103 dereference failure: dead object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.19] line 103 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.20] line 103 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.21] line 103 dereference failure: invalid integer address in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.22] line 103 dereference failure: pointer invalid in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.23] line 103 dereference failure: pointer NULL in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.24] line 103 dereference failure: deallocated dynamic object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.25] line 103 dereference failure: dead object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.26] line 103 dereference failure: pointer outside dynamic object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.27] line 103 dereference failure: pointer outside object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.28] line 103 dereference failure: invalid integer address in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.29] line 104 dereference failure: pointer invalid in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.30] line 104 dereference failure: pointer NULL in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.31] line 104 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.32] line 104 dereference failure: dead object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.33] line 104 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.34] line 104 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.35] line 104 dereference failure: invalid integer address in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.36] line 104 dereference failure: pointer invalid in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.37] line 104 dereference failure: pointer NULL in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.38] line 104 dereference failure: deallocated dynamic object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.39] line 104 dereference failure: dead object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.40] line 104 dereference failure: pointer outside dynamic object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.41] line 104 dereference failure: pointer outside object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.42] line 104 dereference failure: invalid integer address in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.43] line 109 dereference failure: pointer invalid in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.44] line 109 dereference failure: pointer NULL in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.45] line 109 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.46] line 109 dereference failure: dead object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.47] line 109 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.48] line 109 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.49] line 109 dereference failure: invalid integer address in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.50] line 109 dereference failure: pointer invalid in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.51] line 109 dereference failure: pointer NULL in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.52] line 109 dereference failure: deallocated dynamic object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.53] line 109 dereference failure: dead object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.54] line 109 dereference failure: pointer outside dynamic object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.55] line 109 dereference failure: pointer outside object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.56] line 109 dereference failure: invalid integer address in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.57] line 111 dereference failure: pointer invalid in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.58] line 111 dereference failure: pointer NULL in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.59] line 111 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.60] line 111 dereference failure: dead object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.61] line 111 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.62] line 111 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.63] line 111 dereference failure: invalid integer address in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.64] line 111 dereference failure: pointer invalid in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.65] line 111 dereference failure: pointer NULL in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.66] line 111 dereference failure: deallocated dynamic object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.67] line 111 dereference failure: dead object in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.68] line 111 dereference failure: pointer outside dynamic object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.69] line 111 dereference failure: pointer outside object bounds in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.70] line 111 dereference failure: invalid integer address in *allocated: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.71] line 115 dereference failure: pointer invalid in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.72] line 115 dereference failure: pointer NULL in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.73] line 115 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.74] line 115 dereference failure: dead object in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.75] line 115 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.76] line 115 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[s2n_mem_malloc_mlock_impl.pointer_dereference.77] line 115 dereference failure: invalid integer address in *ptr: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_mem_malloc_no_mlock_impl
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.1] line 122 dereference failure: pointer invalid in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.2] line 122 dereference failure: pointer NULL in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.3] line 122 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.4] line 122 dereference failure: dead object in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.5] line 122 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.6] line 122 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.7] line 122 dereference failure: invalid integer address in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.8] line 123 dereference failure: pointer invalid in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.9] line 123 dereference failure: pointer NULL in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.10] line 123 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.11] line 123 dereference failure: dead object in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.12] line 123 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.13] line 123 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.14] line 123 dereference failure: invalid integer address in *ptr: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.15] line 124 dereference failure: pointer invalid in *allocated: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.16] line 124 dereference failure: pointer NULL in *allocated: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.17] line 124 dereference failure: deallocated dynamic object in *allocated: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.18] line 124 dereference failure: dead object in *allocated: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.19] line 124 dereference failure: pointer outside dynamic object bounds in *allocated: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.20] line 124 dereference failure: pointer outside object bounds in *allocated: SUCCESS
[s2n_mem_malloc_no_mlock_impl.pointer_dereference.21] line 124 dereference failure: invalid integer address in *allocated: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_mem.c function s2n_realloc
[s2n_realloc.overflow.1] line 170 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)b): SUCCESS
[s2n_realloc.overflow.2] line 170 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)b) + sizeof(struct s2n_blob) /*24ul*/ : SUCCESS
[s2n_realloc.overflow.3] line 170 arithmetic overflow on signed to unsigned type conversion in (unsigned long int)POINTER_OFFSET((const void *)b): SUCCESS
[s2n_realloc.overflow.4] line 170 arithmetic overflow on unsigned + in (unsigned long int)POINTER_OFFSET((const void *)b) + sizeof(struct s2n_blob) /*24ul*/ : SUCCESS
[s2n_realloc.pointer_dereference.1] line 177 dereference failure: pointer invalid in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.2] line 177 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.3] line 177 dereference failure: deallocated dynamic object in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.4] line 177 dereference failure: dead object in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.5] line 177 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.6] line 177 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.7] line 177 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.8] line 179 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.9] line 179 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.10] line 179 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_realloc.overflow.5] line 182 arithmetic overflow on unsigned - in b->size - size: SUCCESS
[s2n_realloc.pointer_dereference.11] line 182 dereference failure: pointer invalid in b->size: SUCCESS
[s2n_realloc.pointer_dereference.12] line 182 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_realloc.pointer_dereference.13] line 182 dereference failure: deallocated dynamic object in b->size: SUCCESS
[s2n_realloc.pointer_dereference.14] line 182 dereference failure: dead object in b->size: SUCCESS
[s2n_realloc.pointer_dereference.15] line 182 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.16] line 182 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.17] line 182 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_realloc.pointer_dereference.18] line 186 dereference failure: pointer invalid in b->size: SUCCESS
[s2n_realloc.pointer_dereference.19] line 186 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_realloc.pointer_dereference.20] line 186 dereference failure: deallocated dynamic object in b->size: SUCCESS
[s2n_realloc.pointer_dereference.21] line 186 dereference failure: dead object in b->size: SUCCESS
[s2n_realloc.pointer_dereference.22] line 186 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.23] line 186 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.24] line 186 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_realloc.pointer_dereference.25] line 191 dereference failure: pointer invalid in s2n_mem_malloc_cb: SUCCESS
[s2n_realloc.pointer_dereference.26] line 191 dereference failure: pointer NULL in s2n_mem_malloc_cb: SUCCESS
[s2n_realloc.pointer_dereference.27] line 191 dereference failure: deallocated dynamic object in s2n_mem_malloc_cb: SUCCESS
[s2n_realloc.pointer_dereference.28] line 191 dereference failure: dead object in s2n_mem_malloc_cb: SUCCESS
[s2n_realloc.pointer_dereference.29] line 191 dereference failure: pointer outside dynamic object bounds in s2n_mem_malloc_cb: SUCCESS
[s2n_realloc.pointer_dereference.30] line 191 dereference failure: pointer outside object bounds in s2n_mem_malloc_cb: SUCCESS
[s2n_realloc.pointer_dereference.31] line 191 dereference failure: invalid integer address in s2n_mem_malloc_cb: SUCCESS
[s2n_realloc.pointer_dereference.32] line 198 dereference failure: pointer invalid in b->size: SUCCESS
[s2n_realloc.pointer_dereference.33] line 198 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_realloc.pointer_dereference.34] line 198 dereference failure: deallocated dynamic object in b->size: SUCCESS
[s2n_realloc.pointer_dereference.35] line 198 dereference failure: dead object in b->size: SUCCESS
[s2n_realloc.pointer_dereference.36] line 198 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.37] line 198 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.38] line 198 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_realloc.pointer_dereference.39] line 199 dereference failure: pointer invalid in b->size: SUCCESS
[s2n_realloc.pointer_dereference.40] line 199 dereference failure: pointer NULL in b->size: SUCCESS
[s2n_realloc.pointer_dereference.41] line 199 dereference failure: deallocated dynamic object in b->size: SUCCESS
[s2n_realloc.pointer_dereference.42] line 199 dereference failure: dead object in b->size: SUCCESS
[s2n_realloc.pointer_dereference.43] line 199 dereference failure: pointer outside dynamic object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.44] line 199 dereference failure: pointer outside object bounds in b->size: SUCCESS
[s2n_realloc.pointer_dereference.45] line 199 dereference failure: invalid integer address in b->size: SUCCESS
[s2n_realloc.pointer_dereference.46] line 199 dereference failure: pointer NULL in b->data: SUCCESS
[s2n_realloc.pointer_dereference.47] line 199 dereference failure: pointer outside dynamic object bounds in b->data: SUCCESS
[s2n_realloc.pointer_dereference.48] line 199 dereference failure: pointer outside object bounds in b->data: SUCCESS
[s2n_realloc.pointer_dereference.49] line 199 dereference failure: invalid integer address in b->data: SUCCESS
[s2n_realloc.pointer_dereference.50] line 202 dereference failure: pointer invalid in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.51] line 202 dereference failure: pointer NULL in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.52] line 202 dereference failure: deallocated dynamic object in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.53] line 202 dereference failure: dead object in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.54] line 202 dereference failure: pointer outside dynamic object bounds in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.55] line 202 dereference failure: pointer outside object bounds in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.56] line 202 dereference failure: invalid integer address in b->allocated: SUCCESS
[s2n_realloc.pointer_dereference.57] line 206 dereference failure: pointer invalid in *b: SUCCESS
[s2n_realloc.pointer_dereference.58] line 206 dereference failure: pointer NULL in *b: SUCCESS
[s2n_realloc.pointer_dereference.59] line 206 dereference failure: deallocated dynamic object in *b: SUCCESS
[s2n_realloc.pointer_dereference.60] line 206 dereference failure: dead object in *b: SUCCESS
[s2n_realloc.pointer_dereference.61] line 206 dereference failure: pointer outside dynamic object bounds in *b: SUCCESS
[s2n_realloc.pointer_dereference.62] line 206 dereference failure: pointer outside object bounds in *b: SUCCESS
[s2n_realloc.pointer_dereference.63] line 206 dereference failure: invalid integer address in *b: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_safety.c function s2n_align_to
[s2n_align_to.pointer_dereference.1] line 179 dereference failure: pointer invalid in *out: SUCCESS
[s2n_align_to.pointer_dereference.2] line 179 dereference failure: pointer NULL in *out: SUCCESS
[s2n_align_to.pointer_dereference.3] line 179 dereference failure: deallocated dynamic object in *out: SUCCESS
[s2n_align_to.pointer_dereference.4] line 179 dereference failure: dead object in *out: SUCCESS
[s2n_align_to.pointer_dereference.5] line 179 dereference failure: pointer outside dynamic object bounds in *out: SUCCESS
[s2n_align_to.pointer_dereference.6] line 179 dereference failure: pointer outside object bounds in *out: SUCCESS
[s2n_align_to.pointer_dereference.7] line 179 dereference failure: invalid integer address in *out: SUCCESS
[s2n_align_to.division-by-zero.1] line 184 division by zero in (i - (unsigned long int)1) / a: SUCCESS
[s2n_align_to.overflow.1] line 184 arithmetic overflow on unsigned - in i - (unsigned long int)1: SUCCESS
[s2n_align_to.overflow.2] line 184 arithmetic overflow on unsigned + in (i - (unsigned long int)1) / a + (unsigned long int)1: SUCCESS
[s2n_align_to.overflow.3] line 184 arithmetic overflow on unsigned * in a * ((i - (unsigned long int)1) / a + (unsigned long int)1): SUCCESS
[s2n_align_to.overflow.4] line 186 arithmetic overflow on unsigned to unsigned type conversion in (uint32_t)result: SUCCESS
[s2n_align_to.pointer_dereference.8] line 186 dereference failure: pointer invalid in *out: SUCCESS
[s2n_align_to.pointer_dereference.9] line 186 dereference failure: pointer NULL in *out: SUCCESS
[s2n_align_to.pointer_dereference.10] line 186 dereference failure: deallocated dynamic object in *out: SUCCESS
[s2n_align_to.pointer_dereference.11] line 186 dereference failure: dead object in *out: SUCCESS
[s2n_align_to.pointer_dereference.12] line 186 dereference failure: pointer outside dynamic object bounds in *out: SUCCESS
[s2n_align_to.pointer_dereference.13] line 186 dereference failure: pointer outside object bounds in *out: SUCCESS
[s2n_align_to.pointer_dereference.14] line 186 dereference failure: invalid integer address in *out: SUCCESS
/home/tspriggs/Development/s2n/utils/s2n_safety.c function s2n_mul_overflow
[s2n_mul_overflow.overflow.1] line 169 arithmetic overflow on unsigned * in (uint64_t)a * (uint64_t)b: SUCCESS
[s2n_mul_overflow.overflow.2] line 171 arithmetic overflow on unsigned to unsigned type conversion in (uint32_t)result: SUCCESS
[s2n_mul_overflow.pointer_dereference.1] line 171 dereference failure: pointer invalid in *out: SUCCESS
[s2n_mul_overflow.pointer_dereference.2] line 171 dereference failure: pointer NULL in *out: SUCCESS
[s2n_mul_overflow.pointer_dereference.3] line 171 dereference failure: deallocated dynamic object in *out: SUCCESS
[s2n_mul_overflow.pointer_dereference.4] line 171 dereference failure: dead object in *out: SUCCESS
[s2n_mul_overflow.pointer_dereference.5] line 171 dereference failure: pointer outside dynamic object bounds in *out: SUCCESS
[s2n_mul_overflow.pointer_dereference.6] line 171 dereference failure: pointer outside object bounds in *out: SUCCESS
[s2n_mul_overflow.pointer_dereference.7] line 171 dereference failure: invalid integer address in *out: SUCCESS
function getenv
[getenv.pointer_dereference.1] line 18 dereference failure: pointer invalid in *name: SUCCESS
[getenv.pointer_dereference.2] line 18 dereference failure: pointer NULL in *name: SUCCESS
[getenv.pointer_dereference.3] line 18 dereference failure: deallocated dynamic object in *name: SUCCESS
[getenv.pointer_dereference.4] line 18 dereference failure: dead object in *name: SUCCESS
[getenv.pointer_dereference.5] line 18 dereference failure: pointer outside dynamic object bounds in *name: SUCCESS
[getenv.pointer_dereference.6] line 18 dereference failure: pointer outside object bounds in *name: SUCCESS
[getenv.pointer_dereference.7] line 18 dereference failure: invalid integer address in *name: SUCCESS
[getenv.overflow.1] line 43 arithmetic overflow on unsigned - in buf_size - (unsigned long int)1: SUCCESS
[getenv.overflow.2] line 43 arithmetic overflow on unsigned to signed type conversion in (signed long int)(buf_size - (unsigned long int)1): SUCCESS
[getenv.overflow.3] line 43 pointer arithmetic overflow on + in buffer + (signed long int)(buf_size - (unsigned long int)1): SUCCESS
[getenv.pointer_dereference.8] line 43 dereference failure: pointer invalid in buffer[(signed long int)(buf_size - (unsigned long int)1)]: SUCCESS
[getenv.pointer_dereference.9] line 43 dereference failure: pointer NULL in buffer[(signed long int)(buf_size - (unsigned long int)1)]: SUCCESS
[getenv.pointer_dereference.10] line 43 dereference failure: deallocated dynamic object in buffer[(signed long int)(buf_size - (unsigned long int)1)]: SUCCESS
[getenv.pointer_dereference.11] line 43 dereference failure: dead object in buffer[(signed long int)(buf_size - (unsigned long int)1)]: SUCCESS
[getenv.pointer_dereference.12] line 43 dereference failure: pointer outside dynamic object bounds in buffer[(signed long int)(buf_size - (unsigned long int)1)]: SUCCESS
[getenv.pointer_dereference.13] line 43 dereference failure: pointer outside object bounds in buffer[(signed long int)(buf_size - (unsigned long int)1)]: SUCCESS
[getenv.pointer_dereference.14] line 43 dereference failure: invalid integer address in buffer[(signed long int)(buf_size - (unsigned long int)1)]: SUCCESS
function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS
function posix_memalign
[posix_memalign.overflow.1] line 18 arithmetic overflow on unsigned - in multiplier - (unsigned long int)1: SUCCESS
[posix_memalign.pointer_dereference.1] line 41 dereference failure: pointer invalid in *ptr: SUCCESS
[posix_memalign.pointer_dereference.2] line 41 dereference failure: pointer NULL in *ptr: SUCCESS
[posix_memalign.pointer_dereference.3] line 41 dereference failure: deallocated dynamic object in *ptr: SUCCESS
[posix_memalign.pointer_dereference.4] line 41 dereference failure: dead object in *ptr: SUCCESS
[posix_memalign.pointer_dereference.5] line 41 dereference failure: pointer outside dynamic object bounds in *ptr: SUCCESS
[posix_memalign.pointer_dereference.6] line 41 dereference failure: pointer outside object bounds in *ptr: SUCCESS
[posix_memalign.pointer_dereference.7] line 41 dereference failure: invalid integer address in *ptr: SUCCESS
s2n_array_new_harness.c function s2n_array_new_harness
[s2n_array_new_harness.assertion.1] line 39 assertion S2N_IMPLIES(new_array != NULL, s2n_array_is_valid(new_array)): SUCCESS
VERIFICATION SUCCESSFUL
```
CBMC version: 5.12 (cbmc-5.12.1-10-gdf2638c59) Operating system: macOS Mojave Version 10.14.6 Exact command line resulting in the issue: Run
s2n_array_new
proof. What behaviour did you expect: Verification Successful. What happened instead: Invariant check failed.To reproduce the error, clone cbmc-array-set-predicates branch and go to
s2n/tests/cbmc/proofs/s2n_array_new
dir. To run the proof harness, just entermake cbmc
(you needgoto-cc
,goto-instrument
,goto-analyzer
, andcbmc
on your$PATH
). I got the following error message: