Skip to content

Invariant check failed when using memset #5389

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
feliperodri opened this issue Jun 22, 2020 · 1 comment · Fixed by #5390
Closed

Invariant check failed when using memset #5389

feliperodri opened this issue Jun 22, 2020 · 1 comment · Fixed by #5390
Labels
aws Bugs or features of importance to AWS CBMC users

Comments

@feliperodri
Copy link
Collaborator

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:

--- begin invariant violation report ---
Invariant check failed
File: flattening/boolbv_extractbits.cpp:37 function: convert_extractbits
Condition: upper end of extracted bits must be within the bitvector
Reason: upper_as_int >= 0 && upper_as_int < src_bv.size()
Backtrace:
0   cbmc                                0x000000010229f8ea _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x000000010229fe92 _Z13get_backtracev + 210
2   cbmc                                0x00000001022c3140 _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 48
3   cbmc                                0x00000001020ffe88 _Z24report_invariant_failureIJRK16source_locationt24irep_pretty_diagnosticstEEvRKNSt3__112basic_stringIcNS4_11char_traitsIcEENS4_9allocatorIcEEEESC_iSA_SA_DpOT_ + 72
4   cbmc                                0x0000000102114c8f _ZN7boolbvt19convert_extractbitsERK17extractbits_exprt + 2031
5   cbmc                                0x0000000102100537 _ZN7boolbvt17convert_bitvectorERK5exprt + 1575
6   cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
7   cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
8   cbmc                                0x000000010211b71d _ZN7boolbvt10convert_ifERK8if_exprt + 173
9   cbmc                                0x0000000102100221 _ZN7boolbvt17convert_bitvectorERK5exprt + 785
10  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
11  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
12  cbmc                                0x0000000102109953 _ZN7boolbvt15convert_bitwiseERK5exprt + 387
13  cbmc                                0x00000001021005c5 _ZN7boolbvt17convert_bitvectorERK5exprt + 1717
14  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
15  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
16  cbmc                                0x0000000102129726 _ZN7boolbvt19convert_bv_typecastERK14typecast_exprt + 70
17  cbmc                                0x0000000102100275 _ZN7boolbvt17convert_bitvectorERK5exprt + 869
18  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
19  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
20  cbmc                                0x0000000102128677 _ZN7boolbvt14convert_structERK12struct_exprt + 391
21  cbmc                                0x0000000102100717 _ZN7boolbvt17convert_bitvectorERK5exprt + 2055
22  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
23  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
24  cbmc                                0x0000000102128677 _ZN7boolbvt14convert_structERK12struct_exprt + 391
25  cbmc                                0x0000000102100717 _ZN7boolbvt17convert_bitvectorERK5exprt + 2055
26  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
27  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
28  cbmc                                0x000000010210c466 _ZN7boolbvt19convert_byte_updateERK17byte_update_exprt + 182
29  cbmc                                0x00000001021006e7 _ZN7boolbvt17convert_bitvectorERK5exprt + 2007
30  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
31  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
32  cbmc                                0x000000010211b6f7 _ZN7boolbvt10convert_ifERK8if_exprt + 135
33  cbmc                                0x0000000102100221 _ZN7boolbvt17convert_bitvectorERK5exprt + 785
34  cbmc                                0x000000010213a8b0 _ZN12bv_pointerst17convert_bitvectorERK5exprt + 2320
35  cbmc                                0x00000001020ff8de _ZN7boolbvt10convert_bvERK5exprtN6nonstd13optional_lite8optionalImEE + 814
36  cbmc                                0x0000000102104238 _ZN7boolbvt27boolbv_set_equality_to_trueERK11equal_exprt + 200
37  cbmc                                0x0000000102104315 _ZN7boolbvt6set_toERK5exprtb + 101
38  cbmc                                0x00000001020247ec _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 204
39  cbmc                                0x0000000102024495 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 117
40  cbmc                                0x0000000102025ce2 _ZN22symex_target_equationt7convertER19decision_proceduret + 18
41  cbmc                                0x0000000101ecf7d6 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 342
42  cbmc                                0x0000000101ed16a9 _Z24prepare_property_deciderRNSt3__113unordered_mapI8dstringt14property_infotNS_4hashIS1_EENS_8equal_toIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 441
43  cbmc                                0x0000000101ed9288 _ZN25multi_path_symex_checkertclERNSt3__113unordered_mapI8dstringt14property_infotNS0_4hashIS2_EENS0_8equal_toIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 264
44  cbmc                                0x0000000102342237 _ZN40cover_goals_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 87
45  cbmc                                0x000000010234047d _ZN19cbmc_parse_optionst4doitEv + 3565
46  cbmc                                0x00000001022b94e2 _ZN19parse_options_baset4mainEv + 242
47  cbmc                                0x000000010233b7f8 main + 40
48  libdyld.dylib                       0x00007fff5d05d3d5 start + 1
49  ???                                 0x000000000000000b 0x0 + 11

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
source location: 
extractbits
  * type: bv
      * width: 8
  0: typecast
      * type: bv
          * width: 1
      0: symbol
          * type: c_bit_field
              * #source_location: 
                * file: /Users/felisous/Documents/aws/crypto/s2n/utils/s2n_blob.h
                * line: 37
                * function: 
                * working_directory: /Users/felisous/Documents/aws/crypto/s2n/tests/cbmc/proofs/s2n_array_new
              * width: 1
              0: unsignedbv
                  * width: 32
                  * #c_type: unsigned_int
          * identifier: symex_dynamic::dynamic_object3#29..mem..growable
          * expression: member
              * type: c_bit_field
                  * #source_location: 
                    * file: /Users/felisous/Documents/aws/crypto/s2n/utils/s2n_blob.h
                    * line: 37
                    * function: 
                    * working_directory: /Users/felisous/Documents/aws/crypto/s2n/tests/cbmc/proofs/s2n_array_new
                  * width: 1
                  0: unsignedbv
                      * width: 32
                      * #c_type: unsigned_int
              * component_name: growable
              0: member
                  * type: struct_tag
                      * #source_location: 
                        * file: /Users/felisous/Documents/aws/crypto/s2n/utils/s2n_array.c
                        * line: 47
                        * function: s2n_array_new
                        * working_directory: /Users/felisous/Documents/aws/crypto/s2n/tests/cbmc/proofs/s2n_array_new
                      * identifier: tag-s2n_blob
                  * component_name: mem
                  0: symbol
                      * type: struct_tag
                          * #source_location: 
                            * file: s2n_array_new_harness.c
                            * line: 36
                            * function: s2n_array_new_harness
                            * working_directory: /Users/felisous/Documents/aws/crypto/s2n/tests/cbmc/proofs/s2n_array_new
                          * identifier: tag-s2n_array
                      * identifier: symex_dynamic::dynamic_object3
          * #SSA_symbol: 1
          * L2: 29
          * L1_object_identifier: symex_dynamic::dynamic_object3..mem..growable
  1: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 7
  2: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 0
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
@karkhaz karkhaz added the aws Bugs or features of importance to AWS CBMC users label Jun 22, 2020
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jun 23, 2020
@tautschnig
Byte-update lowering: handle sub-byte sized bit fields
efed351 
Extend the value to be updated to the update size immediately to avoid
extractbits operations that attempt to extract bits that do not exist.

Fixes: diffblue#5389
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jun 23, 2020
@tautschnig
Byte-update lowering: handle sub-byte sized bit fields
54411e0 
Extend the value to be updated to the update size immediately to avoid
extractbits operations that attempt to extract bits that do not exist.

Fixes: diffblue#5389
@tautschnig tautschnig mentioned this issue Jun 23, 2020
Merged
3 tasks
@thomasspriggs
Copy link
Contributor

thomasspriggs commented Jul 9, 2020 •
edited by hannes-steffenhagen-diffblue
Loading

Unable to reproduce on Ubuntu 20 -

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

<builtin-library-getenv> 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

<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS

<builtin-library-posix_memalign> 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

tautschnig added a commit to tautschnig/cbmc that referenced this issue Nov 6, 2020
@tautschnig
Byte-update lowering: handle sub-byte sized bit fields
ee1f966 
Extend the value to be updated to the update size immediately to avoid
extractbits operations that attempt to extract bits that do not exist.

Fixes: diffblue#5389
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
aws Bugs or features of importance to AWS CBMC users
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Byte-update lowering: handle sub-byte sized bit fields tautschnig/cbmc
3 participants
@karkhaz @feliperodri @thomasspriggs