CBMC version 5.6 64-bit x86_64 linux
Parsing json.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking json
Generating GOTO Program
Adding CPROVER library (x86_64)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Instrumenting coverage goals
Starting Bounded Model Checking
Unwinding loop skip_space.0 iteration 1 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 2 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 3 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 4 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 5 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 6 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 7 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 8 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 9 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 10 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 11 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 12 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 13 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 14 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 15 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 16 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 17 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 18 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 19 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 20 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 21 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 22 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 23 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 24 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 25 file json.c line 974 function skip_space thread 0
Unwinding loop expect_literal.0 iteration 1 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 2 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 3 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 4 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 1 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 2 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 3 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 4 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 5 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 1 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 2 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 3 file json.c line 1265 function expect_literal thread 0
Unwinding loop expect_literal.0 iteration 4 file json.c line 1265 function expect_literal thread 0
Unwinding loop sb_grow.0 iteration 1 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 2 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 3 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 4 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 5 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 6 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 7 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 8 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 9 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 10 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 11 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 12 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 13 file json.c line 83 function sb_grow thread 0
Unwinding loop sb_grow.0 iteration 1 file json.c line 83 function sb_grow thread 0
Unwinding loop parse_string.3 iteration 1 file json.c line 817 function parse_string thread 0
Unwinding loop sb_finish.0 iteration 1 file json.c line 113 function sb_finish thread 0
Unwinding loop sb_finish.0 iteration 2 file json.c line 113 function sb_finish thread 0
Unwinding loop sb_finish.0 iteration 3 file json.c line 113 function sb_finish thread 0
Unwinding loop sb_finish.0 iteration 4 file json.c line 113 function sb_finish thread 0
Unwinding loop skip_space.0 iteration 1 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 2 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 1 file json.c line 974 function skip_space thread 0
Unwinding loop parse_number.32767 iteration 1 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 2 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 3 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 4 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 5 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 6 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 7 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 8 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 9 file json.c line 939 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 1 file json.c line 949 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 2 file json.c line 949 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 3 file json.c line 949 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 4 file json.c line 949 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 5 file json.c line 949 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 6 file json.c line 949 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 7 file json.c line 949 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 8 file json.c line 949 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 1 file json.c line 961 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 2 file json.c line 961 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 3 file json.c line 961 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 4 file json.c line 961 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 5 file json.c line 961 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 6 file json.c line 961 function parse_number thread 0
Unwinding loop parse_number.32767 iteration 7 file json.c line 961 function parse_number thread 0
**** WARNING: no body for function strtod
Unwinding loop skip_space.0 iteration 1 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 2 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 3 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 4 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 5 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 6 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 7 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 8 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 9 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 10 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 11 file json.c line 974 function skip_space thread 0
Unwinding loop skip_space.0 iteration 12 file json.c line 974 function skip_space thread 0
Unwinding recursion json_delete iteration 1
Unwinding loop json_delete.0 iteration 1 file json.c line 425 function json_delete thread 0
Unwinding recursion json_delete iteration 1
Unwinding loop json_delete.0 iteration 2 file json.c line 425 function json_delete thread 0
size of program expression: 4552 steps
Generated 784 VCC(s), 784 remaining after simplification
Passing problem to propositional reduction
converting SSA
byte_extract flatting with non-constant size: byte_extract_little_endian
  * type: array
      * size: symbol
          * type: unsignedbv
              * width: 64
              * #source_location: 
                * file: <built-in-additions>
                * line: 1
                * working_directory: /home/tkiley/workspace/C/jo
              * #c_type: unsigned_long_int
          * identifier: symex_dynamic::dynamic_object_size7#1
          * expression: symbol
              * type: unsignedbv
                  * width: 64
                  * #source_location: 
                    * file: <built-in-additions>
                    * line: 1
                    * working_directory: /home/tkiley/workspace/C/jo
                  * #c_type: unsigned_long_int
              * identifier: symex_dynamic::dynamic_object_size7
          * L2: 1
          * #SSA_symbol: 1
      * #dynamic: 1
      0: unsignedbv
          * width: 8
          * #c_type: unsigned_char
  0: symbol
      * type: array
          * size: constant
              * type: unsignedbv
                  * width: 64
                  * #source_location: 
                    * file: <built-in-additions>
                    * line: 1
                    * working_directory: /home/tkiley/workspace/C/jo
                  * #c_type: unsigned_long_int
              * value: 0000000000000000000000000000000000000000000000000000000000010001
          * #dynamic: 1
          0: unsignedbv
              * width: 8
              * #c_type: unsigned_char
      * identifier: symex_dynamic::dynamic_object4#0
      * expression: symbol
          * type: array
              * size: constant
                  * type: unsignedbv
                      * width: 64
                      * #source_location: 
                        * file: <built-in-additions>
                        * line: 1
                        * working_directory: /home/tkiley/workspace/C/jo
                      * #c_type: unsigned_long_int
                  * value: 0000000000000000000000000000000000000000000000000000000000010001
              * #dynamic: 1
              0: unsignedbv
                  * width: 8
                  * #c_type: unsigned_char
          * identifier: symex_dynamic::dynamic_object4
      * L2: 0
      * #SSA_symbol: 1
  1: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 0000000000000000000000000000000000000000000000000000000000000000