byte_update of unknown width error

[guyio]

Hey, I've been trying to reproduce a bug example of an integer overflow used for an allocation.
Using cbmc I've found that I get the following error:
file cve-2017-5428.c line 49: byte_update of unknown width

Version 5.9 on windows.
command line used:
cbmc cve-2017-5428.c --function main --bounds-check --pointer-check

output:
CBMC version 5.9 (cbmc-5.9) 64-bit x86_64 windows
Parsing cve-2017-5428.c
cve-2017-5428.c
Converting
Type-checking cve-2017-5428
Generating GOTO Program
Adding CPROVER library (x86_64)
tmp.stdin10904.ADlaaa.c
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 256 steps
simple slicing removed 25 assignments
Generated 123 VCC(s), 71 remaining after simplification
Passing problem to propositional reduction
converting SSA
file cve-2017-5428.c line 49: byte_update of unknown width:
byte_update_little_endian

• type: array
  • size: symbol
    • type: unsignedbv
      • width: 64
      • #source_location:
        • file:
        • line: 1
        • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
      • #typedef: __CPROVER_size_t
      • #c_type: unsigned_long_long_int
    • identifier: symex_dynamic::dynamic_object_size1!0#1
    • expression: symbol
      • type: unsignedbv
        • width: 64
        • #source_location:
          • file:
          • line: 1
          • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
        • #typedef: __CPROVER_size_t
        • #c_type: unsigned_long_long_int
      • identifier: symex_dynamic::dynamic_object_size1
    • L0: 0
    • L2: 1
    • L1_object_identifier: symex_dynamic::dynamic_object_size1!0
    • #SSA_symbol: 1
  • #dynamic: 1
    0: unsignedbv
    • width: 8
    • #typedef: uint8_t
    • #c_type: unsigned_char
      0: symbol
  • type: array
    • size: symbol
      • type: unsignedbv
        • width: 64
        • #source_location:
          • file:
          • line: 1
          • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
        • #typedef: __CPROVER_size_t
        • #c_type: unsigned_long_long_int
      • identifier: symex_dynamic::dynamic_object_size1!0#1
      • expression: symbol
        • type: unsignedbv
          • width: 64
          • #source_location:
            • file:
            • line: 1
            • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
          • #typedef: __CPROVER_size_t
          • #c_type: unsigned_long_long_int
        • identifier: symex_dynamic::dynamic_object_size1
      • L0: 0
      • L2: 1
      • L1_object_identifier: symex_dynamic::dynamic_object_size1!0
      • #SSA_symbol: 1
    • #dynamic: 1
      0: unsignedbv
      • width: 8
      • #typedef: uint8_t
      • #c_type: unsigned_char
  • identifier: symex_dynamic::dynamic_object1#1
  • expression: symbol
    • type: array
      • size: symbol
        • type: unsignedbv
          • width: 64
          • #source_location:
            • file:
            • line: 1
            • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
          • #typedef: __CPROVER_size_t
          • #c_type: unsigned_long_long_int
        • identifier: symex_dynamic::dynamic_object_size1!0#1
        • expression: symbol
          • type: unsignedbv
            • width: 64
            • #source_location:
              • file:
              • line: 1
              • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
            • #typedef: __CPROVER_size_t
            • #c_type: unsigned_long_long_int
          • identifier: symex_dynamic::dynamic_object_size1
        • L0: 0
        • L2: 1
        • L1_object_identifier: symex_dynamic::dynamic_object_size1!0
        • #SSA_symbol: 1
      • #dynamic: 1
        0: unsignedbv
        • width: 8
        • #typedef: uint8_t
        • #c_type: unsigned_char
    • identifier: symex_dynamic::dynamic_object1
  • L2: 1
  • L1_object_identifier: symex_dynamic::dynamic_object1
  • #SSA_symbol: 1
    1: constant
  • type: signedbv
    • width: 64
    • #c_type: signed_long_long_int
  • value: 0000000000000000000000000000000000000000000000000000000000000000
    2: symbol
  • type: array
    • size: symbol
      • type: signedbv
        • width: 64
        • #c_type: signed_long_long_int
      • identifier: memcpy::1::1::src_n$array_size0!0@1#2
      • expression: symbol
        • type: signedbv
          • width: 64
          • #c_type: signed_long_long_int
        • identifier: memcpy::1::1::src_n$array_size0
      • L0: 0
      • L1: 1
      • L2: 2
      • L1_object_identifier: memcpy::1::1::src_n$array_size0!0@1
      • #SSA_symbol: 1
    • #source_location:
      • file:
      • line: 39
      • function: memcpy
      • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
        0: signedbv
        • width: 8
        • #c_type: char
  • identifier: memcpy::1::1::src_n!0@1#2
  • expression: symbol
    • type: array
      • size: symbol
        • type: signedbv
          • width: 64
          • #c_type: signed_long_long_int
        • identifier: memcpy::1::1::src_n$array_size0!0@1#2
        • expression: symbol
          • type: signedbv
            • width: 64
            • #c_type: signed_long_long_int
          • identifier: memcpy::1::1::src_n$array_size0
        • L0: 0
        • L1: 1
        • L2: 2
        • L1_object_identifier: memcpy::1::1::src_n$array_size0!0@1
        • #SSA_symbol: 1
      • #source_location:
        • file:
        • line: 39
        • function: memcpy
        • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
          0: signedbv
          • width: 8
          • #c_type: char
    • identifier: memcpy::1::1::src_n
    • #source_location:
      • file:
      • line: 39
      • function: memcpy
      • working_directory: C:\Users\guyi\Downloads\cbmc-5-9-win
  • L0: 0
  • L1: 1
  • L2: 2
  • L1_object_identifier: memcpy::1::1::src_n!0@1
  • #SSA_symbol: 1

Is that a known issue? or should I investigate?

attached input c file:
cve-2017-5428.txt

[tautschnig]

Thank you very much for this bug report. This is a problem the fix of which is work in progress; as a temporary workaround you might want to enable the loop-based version of memcpy in src/ansi-c/library/string.c (the line saying for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];) and instead comment out the three lines below that.

[guyio]

Thank you!

[jkbbwr]

@tautschnig Has there been any progress on the fix for this?

[tautschnig]

The byte-update problem has since been fixed, but now we run into "array too large for flattening." This requires #1874 and #2108.