indirect leak in `irept::detach`

[mgudemann]

after #528 / #568
the following asan erreror are reported

=================================================================
==31813==ERROR: LeakSanitizer: detected memory leaks

Indirect leak of 270336 byte(s) in 2112 object(s) allocated from:
    #0 0x7f9c83381532 in operator new(unsigned long) (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x99532)
    #1 0x5c3c94 in irept::detach() /home/guedemann/source/diffBlue/cbmc/src/util/irep.cpp:113

Indirect leak of 16896 byte(s) in 2112 object(s) allocated from:
    #0 0x7f9c83381532 in operator new(unsigned long) (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x99532)
    #1 0x5c42f7 in __gnu_cxx::new_allocator<irept>::allocate(unsigned long, void const*) /usr/include/c++/5/ext/new_allocator.h:104
    #2 0x5c42f7 in std::allocator_traits<std::allocator<irept> >::allocate(std::allocator<irept>&, unsigned long) /usr/include/c++/5/bits/alloc_traits.h:491
    #3 0x5c42f7 in std::_Vector_base<irept, std::allocator<irept> >::_M_allocate(unsigned long) /usr/include/c++/5/bits/stl_vector.h:170
    #4 0x5c42f7 in std::_Vector_base<irept, std::allocator<irept> >::_M_create_storage(unsigned long) /usr/include/c++/5/bits/stl_vector.h:185
    #5 0x5c42f7 in std::_Vector_base<irept, std::allocator<irept> >::_Vector_base(unsigned long, std::allocator<irept> const&) /usr/include/c++/5/bits/stl_vector.h:136
    #6 0x5c42f7 in std::vector<irept, std::allocator<irept> >::vector(std::vector<irept, std::allocator<irept> > const&) /usr/include/c++/5/bits/stl_vector.h:320
    #7 0x5c42f7 in irept::dt::dt(irept::dt const&) /home/guedemann/source/diffBlue/cbmc/src/util/irep.h:265
    #8 0x5c42f7 in irept::detach() /home/guedemann/source/diffBlue/cbmc/src/util/irep.cpp:113

SUMMARY: AddressSanitizer: 287232 byte(s) leaked in 4224 allocation(s).
EXIT=23
SIGNAL=0

for the standard regression tests, cbmc-java is not affected, from cpp only ModeC3

[tautschnig]

Just to clarify: is that a newly introduced leak, or is something that has existed before #568?

[mgudemann]

this existed before, the address sanitizer only reports one at a time apparently. I had seen this after my first fix in #528 but had wanted to investigate a bit further.

What's strange is that no direct leak is reported as for the other problem, therefore I am not sure where the exact cause lies. In the former problem, the lost pointer was the direct one and all that was only reachable via that pointer the indirect leak.

Also, the leak does not appear to be triggered in all cases. No regression test in cbmc-java triggers it, only one in cpp and none in k-induction. I will provide a list with OK/KO regression tests here.

[mgudemann]

ansi-c

Running tests
  Running Array_Declarator1/test.desc  [FAILED]
  Running Array_Declarator2/test.desc  [SKIPPED]
  Running Array_Declarator3/test.desc  [SKIPPED]
  Running Array_Declarator4/test.desc  [SKIPPED]
  Running Array_Declarator5/test.desc  [SKIPPED]
  Running Array_Declarator6/test.desc  [SKIPPED]
  Running Array_Declarator7/test.desc  [SKIPPED]
  Running Atomic1/test.desc  [FAILED]
  Running Defines1/test.desc  [FAILED]
  Running Empty_Declaration1/test.desc  [FAILED]
  Running Forward_Declaration1/test.desc  [FAILED]
  Running Forward_Declaration2/test.desc  [OK]
  Running Function_parameters1/test.desc  [FAILED]
  Running Function_parameters2/test.desc  [FAILED]
  Running Function_pointer1/test.desc  [FAILED]
  Running Header_files1/test.desc  [FAILED]
  Running Incomplete_Type1/test.desc  [OK]
  Running Initializer_cast1/test.desc  [FAILED]
  Running KnR1/test.desc  [FAILED]
  Running KnR2/test.desc  [FAILED]
  Running KnR3/test.desc  [FAILED]
  Running Lvalue1/test.desc  [FAILED]
  Running MMX1/test.desc  [FAILED]
  Running MMX2/test.desc  [FAILED]
  Running Multiple/test.desc  [FAILED]
  Running Qualifiers1/test.desc  [FAILED]
  Running Recursive_Structure1/test.desc  [FAILED]
  Running Recursive_Structure2/test.desc  [FAILED]
  Running Struct_Bitfields1/test.desc  [FAILED]
  Running Struct_Enum_Padding1/test.desc  [FAILED]
  Running Struct_Hierarchy1/test.desc  [FAILED]
  Running Struct_Initialization1/test.desc  [SKIPPED]
  Running Struct_Padding2/test.desc  [FAILED]
  Running Struct_Padding3/test.desc  [FAILED]
  Running Struct_Padding4/test.desc  [FAILED]
  Running Struct_Padding5/test.desc  [FAILED]
  Running Struct_Padding6/test.desc  [FAILED]
  Running Transparent_union1/test.desc  [FAILED]
  Running Transparent_union2/test.desc  [FAILED]
  Running Typecast_to_array_ptr1/test.desc  [FAILED]
  Running Typecast_to_union1/test.desc  [FAILED]
  Running Union_Initialization1/test.desc  [FAILED]
  Running Union_Padding1/test.desc  [FAILED]
  Running Universal_characters1/test.desc  [FAILED]
  Running VS_extensions1/test.desc  [FAILED]
  Running Zero_Initialization1/test.desc  [FAILED]
  Running _Alignof1/test.desc  [FAILED]
  Running _Bool1/test.desc  [FAILED]
  Running _Generic1/test.desc  [FAILED]
  Running _Noreturn1/test.desc  [FAILED]
  Running _Static_assert1/test.desc  [FAILED]
  Running arithmetic_right_shift1/test.desc  [FAILED]
  Running array_initialization1/test.desc  [FAILED]
  Running array_initialization2/test.desc  [FAILED]
  Running asm1/test.desc  [FAILED]
  Running asm2/test.desc  [FAILED]
  Running asm3/test.desc  [FAILED]
  Running character_literals1/test.desc  [FAILED]
  Running decl_initialization1/test.desc  [FAILED]
  Running decl_initialization2/test.desc  [FAILED]
  Running enum1/test.desc  [FAILED]
  Running enum2/test.desc  [FAILED]
  Running enum3/test.desc  [FAILED]
  Running enum4/test.desc  [FAILED]
  Running enum5/test.desc  [FAILED]
  Running enum6/test.desc  [FAILED]
  Running enum7/test.desc  [SKIPPED]
  Running enum8/test.desc  [FAILED]
  Running envp1/test.desc  [FAILED]
  Running extern1/test.desc  [FAILED]
  Running extern2/test.desc  [FAILED]
  Running extern_inline1/test.desc  [FAILED]
  Running float_constant1/test.desc  [FAILED]
  Running float_constant2/test.desc  [FAILED]
  Running for_scope1/test.desc  [FAILED]
  Running function_return1/test.desc  [OK]
  Running gcc___auto_type1/test.desc  [FAILED]
  Running gcc_attributes1/test.desc  [FAILED]
  Running gcc_attributes2/test.desc  [FAILED]
  Running gcc_attributes3/test.desc  [FAILED]
  Running gcc_attributes4/test.desc  [FAILED]
  Running gcc_attributes5/test.desc  [SKIPPED]
  Running gcc_attributes6/test.desc  [FAILED]
  Running gcc_attributes7/test.desc  [FAILED]
  Running gcc_attributes8/test.desc  [FAILED]
  Running gcc_attributes9/test.desc  [FAILED]
  Running gcc_builtin_constant_p1/test.desc  [FAILED]
  Running gcc_builtins1/test.desc  [FAILED]
  Running gcc_builtins2/test.desc  [FAILED]
  Running gcc_builtins3/test.desc  [FAILED]
  Running gcc_builtins4/test.desc  [FAILED]
  Running gcc_builtins5/test.desc  [FAILED]
  Running gcc_types_compatible_p1/test.desc  [FAILED]
  Running gcc_types_compatible_p2/test.desc  [FAILED]
  Running gcc_types_compatible_p3/test.desc  [FAILED]
  Running gcc_vector1/test.desc  [FAILED]
  Running integer_constant1/test.desc  [FAILED]
  Running integer_constant2/test.desc  [FAILED]
  Running pointer_arithmetic1/test.desc  [FAILED]
  Running pragma_pack1/test.desc  [FAILED]
  Running pragma_pack2/test.desc  [FAILED]
  Running pragma_pack3/test.desc  [FAILED]
  Running return_void/test.desc  [FAILED]
  Running sizeof1/test.desc  [FAILED]
  Running sizeof2/test.desc  [FAILED]
  Running sizeof3/test.desc  [FAILED]
  Running struct2/test.desc  [FAILED]
  Running struct3/test.desc  [FAILED]
  Running struct5/test.desc  [FAILED]
  Running struct6/test.desc  [FAILED]
  Running struct7/test.desc  [FAILED]
  Running switch1/test.desc  [FAILED]
  Running typedef1/test.desc  [FAILED]
  Running typedef2/test.desc  [FAILED]
  Running typedef_code/test.desc  [FAILED]
  Running typeof1/test.desc  [FAILED]
  Running windows_h_VS_2005/test.desc  [FAILED]
  Running windows_h_VS_2008/test.desc  [FAILED]
  Running windows_h_VS_2010/test.desc  [FAILED]
  Running windows_h_VS_2012/test.desc  [FAILED]
  Running windows_h_VS_2013/test.desc  [FAILED]

Tests failed
  109 of 121 tests failed, 9 tests skipped

cbmc

Running tests
  Running ASHR1/test.desc  [FAILED]
  Running Address_of1/test.desc  [FAILED]
  Running Address_of2/test.desc  [FAILED]
  Running Anonymous_Struct1/test.desc  [FAILED]
  Running Anonymous_Struct2/test.desc  [FAILED]
  Running Anonymous_Struct3/test.desc  [FAILED]
  Running Array_Initialization1/test.desc  [FAILED]
  Running Array_Initialization2/test.desc  [FAILED]
  Running Array_Initialization3/test.desc  [FAILED]
  Running Associativity1/test.desc  [FAILED]
  Running Assumption1/test.desc  [FAILED]
  Running BV_Arithmetic1/test.desc  [FAILED]
  Running BV_Arithmetic2/test.desc  [FAILED]
  Running BV_Arithmetic3/test.desc  [FAILED]
  Running BV_Arithmetic4/test.desc  [FAILED]
  Running BV_Arithmetic5/test.desc  [FAILED]
  Running BV_Arithmetic6/test.desc  [FAILED]
  Running Bitfields1/test.desc  [FAILED]
  Running Bitfields2/test.desc  [FAILED]
  Running Bool1/test.desc  [FAILED]
  Running Bool2/test.desc  [FAILED]
  Running Bool3/test.desc  [FAILED]
  Running Bool4/test.desc  [FAILED]
  Running Boolean_Guards1/test.desc  [FAILED]
  Running Computed-Goto1/test.desc  [FAILED]
  Running Division1/test.desc  [FAILED]
  Running Division2/test.desc  [FAILED]
  Running Double-to-float-no-simp1/test.desc  [FAILED]
  Running Double-to-float-no-simp1-fix1/test.desc  [FAILED]
  Running Double-to-float-no-simp1-fix2/test.desc  [FAILED]
  Running Double-to-float-with-simp1/test.desc  [FAILED]
  Running Ellipsis1/test.desc  [FAILED]
  Running Ellipsis2/test.desc  [FAILED]
  Running Empty_struct1/test.desc  [FAILED]
  Running Endianness1/test.desc  [FAILED]
  Running Endianness2/test.desc  [FAILED]
  Running Endianness3/test.desc  [FAILED]
  Running Endianness4/test.desc  [FAILED]
  Running Endianness5/test.desc  [FAILED]
  Running Endianness6/test.desc  [FAILED]
  Running Endianness7/test.desc  [FAILED]
  Running Endianness8/test.desc  [FAILED]
  Running Endianness9/test.desc  [FAILED]
  Running Error_Label1/test.desc  [FAILED]
  Running Error_Label2/test.desc  [FAILED]
  Running Error_Label3/test.desc  [FAILED]
  Running Eval_Order1/test.desc  [FAILED]
  Running Eval_Order2/test.desc  [SKIPPED]
  Running Exceptions1/test.desc  [FAILED]
  Running Failing_Assert1/test.desc  [FAILED]
  Running Fixedbv1/test.desc  [FAILED]
  Running Fixedbv2/test.desc  [FAILED]
  Running Fixedbv3/test.desc  [FAILED]
  Running Fixedbv4/test.desc  [FAILED]
  Running Fixedbv5/test.desc  [FAILED]
  Running Fixedbv6/test.desc  [FAILED]
  Running Fixedbv7/test.desc  [FAILED]
  Running Fixedbv8/test.desc  [FAILED]
  Running Float-Rounding1/test.desc  [FAILED]
  Running Float-Rounding2/test.desc  [FAILED]
  Running Float-data-dependent-rounding/test.desc  [FAILED]
  Running Float-div1/test.desc  [FAILED]
  Running Float-div2/test.desc  [FAILED]
  Running Float-div3/test.desc  [FAILED]
  Running Float-flags-no-simp1/test.desc  [FAILED]
  Running Float-flags-simp1/test.desc  [FAILED]
  Running Float-no-simp1/test.desc  [FAILED]
  Running Float-no-simp2/test.desc  [FAILED]
  Running Float-no-simp3/test.desc  [FAILED]
  Running Float-no-simp4/test.desc  [FAILED]
  Running Float-no-simp5/test.desc  [FAILED]
  Running Float-no-simp6/test.desc  [FAILED]
  Running Float-no-simp7/test.desc  [FAILED]
  Running Float-no-simp8/test.desc  [FAILED]
  Running Float-no-simp9/test.desc  [FAILED]
  Running Float-overflow1/test.desc  [FAILED]
  Running Float-overflow2/test.desc  [FAILED]
  Running Float-to-double1/test.desc  [FAILED]
  Running Float-to-double2/test.desc  [FAILED]
  Running Float-to-int1/test.desc  [FAILED]
  Running Float-to-int2/test.desc  [FAILED]
  Running Float-to-int3/test.desc  [FAILED]
  Running Float-zero-sum1/test.desc  [FAILED]
  Running Float1/test.desc  [FAILED]
  Running Float11/test.desc  [FAILED]
  Running Float12/test.desc  [FAILED]
  Running Float13/test.desc  [FAILED]
  Running Float14/test.desc  [FAILED]
  Running Float18/test.desc  [FAILED]
  Running Float19/test.desc  [FAILED]
  Running Float2/test.desc  [FAILED]
  Running Float20/test.desc  [FAILED]
  Running Float21/test.desc  [FAILED]
  Running Float22/test.desc  [FAILED]
  Running Float23/test.desc  [FAILED]
  Running Float3/test.desc  [FAILED]
  Running Float4/test.desc  [FAILED]
  Running Float5/test.desc  [FAILED]
  Running Float6/test.desc  [FAILED]
  Running Float7/test.desc  [FAILED]
  Running Float8/test.desc  [FAILED]
  Running Float_lib1/test.desc  [FAILED]
  Running Float_lib2/test.desc  [FAILED]
  Running Free1/test.desc  [FAILED]
  Running Free2/test.desc  [FAILED]
  Running Free3/test.desc  [OK]
  Running Free4/test.desc  [OK]
  Running Function-KnR1/test.desc  [FAILED]
  Running Function1/test.desc  [FAILED]
  Running Function10/test.desc  [FAILED]
  Running Function11/test.desc  [FAILED]
  Running Function12/test.desc  [FAILED]
  Running Function13/test.desc  [FAILED]
  Running Function2/test.desc  [FAILED]
  Running Function3/test.desc  [FAILED]
  Running Function4/test.desc  [FAILED]
  Running Function5/test.desc  [FAILED]
  Running Function6/test.desc  [FAILED]
  Running Function7/test.desc  [FAILED]
  Running Function8/test.desc  [FAILED]
  Running Function9/test.desc  [FAILED]
  Running Function_Eval_Order1/test.desc  [SKIPPED]
  Running Function_Eval_Order2/test.desc  [FAILED]
  Running Function_Parameters1/test.desc  [SKIPPED]
  Running Function_Pointer1/test.desc  [FAILED]
  Running Function_Pointer10/test.desc  [FAILED]
  Running Function_Pointer11/test.desc  [FAILED]
  Running Function_Pointer12/test.desc  [FAILED]
  Running Function_Pointer13/test.desc  [FAILED]
  Running Function_Pointer14/test.desc  [FAILED]
  Running Function_Pointer15/test.desc  [FAILED]
  Running Function_Pointer16/test.desc  [FAILED]
  Running Function_Pointer17/test.desc  [FAILED]
  Running Function_Pointer2/test.desc  [FAILED]
  Running Function_Pointer3/test.desc  [FAILED]
  Running Function_Pointer4/test.desc  [FAILED]
  Running Function_Pointer5/test.desc  [FAILED]
  Running Function_Pointer6/test.desc  [FAILED]
  Running Function_Pointer7/test.desc  [FAILED]
  Running Function_Pointer8/test.desc  [FAILED]
  Running Function_Pointer9/test.desc  [FAILED]
  Running Global_Initialization1/test.desc  [FAILED]
  Running Global_Initialization2/test.desc  [FAILED]
  Running Initialization1/test.desc  [FAILED]
  Running Initialization2/test.desc  [FAILED]
  Running Initialization3/test.desc  [FAILED]
  Running Initialization5/test.desc  [FAILED]
  Running Initialization6/test.desc  [FAILED]
  Running Initialization7/test.desc  [SKIPPED]
  Running Linking1/test.desc  [FAILED]
  Running Linking2/test.desc  [FAILED]
  Running Linking3/test.desc  [FAILED]
  Running Linking4/test.desc  [FAILED]
  Running Linking5/test.desc  [SKIPPED]
  Running Local_out_of_scope1/test.desc  [FAILED]
  Running Local_out_of_scope2/test.desc  [FAILED]
  Running Malloc12/test.desc  [SKIPPED]
  Running Malloc13/test.desc  [SKIPPED]
  Running Malloc14/test.desc  [FAILED]
  Running Malloc15/test.desc  [FAILED]
  Running Malloc16/test.desc  [FAILED]
  Running Malloc17/test.desc  [FAILED]
  Running Malloc18/test.desc  [FAILED]
  Running Malloc19/test.desc  [SKIPPED]
  Running Malloc20/test.desc  [SKIPPED]
  Running Malloc21/test.desc  [FAILED]
  Running Malloc22/test.desc  [FAILED]
  Running Malloc23/test.desc  [FAILED]
  Running Memmove1/test.desc  [FAILED]
  Running Memory_leak1/test.desc  [FAILED]
  Running Memory_leak2/test.desc  [FAILED]
  Running Mod1/test.desc  [FAILED]
  Running Mod2/test.desc  [FAILED]
  Running Multi_Dimensional_Array1/test.desc  [FAILED]
  Running Multi_Dimensional_Array2/test.desc  [FAILED]
  Running Multi_Dimensional_Array3/test.desc  [FAILED]
  Running Multi_Dimensional_Array4/test.desc  [FAILED]
  Running Multi_Dimensional_Array5/test.desc  [FAILED]
  Running Multi_Dimensional_Array6/test.desc  [FAILED]
  Running Multiple_Properties1/test.desc  [FAILED]
  Running Negation1/test.desc  [FAILED]
  Running Negation2/test.desc  [FAILED]
  Running Overflow_Addition1/test.desc  [OK]
  Running Overflow_Multiplication1/test.desc  [FAILED]
  Running Overflow_Subtraction1/test.desc  [FAILED]
  Running Pointer_Arithmetic1/test.desc  [FAILED]
  Running Pointer_Arithmetic10/test.desc  [FAILED]
  Running Pointer_Arithmetic11/test.desc  [FAILED]
  Running Pointer_Arithmetic12/test.desc  [FAILED]
  Running Pointer_Arithmetic13/test.desc  [SKIPPED]
  Running Pointer_Arithmetic2/test.desc  [FAILED]
  Running Pointer_Arithmetic3/test.desc  [FAILED]
  Running Pointer_Arithmetic4/test.desc  [FAILED]
  Running Pointer_Arithmetic5/test.desc  [OK]
  Running Pointer_Arithmetic6/test.desc  [FAILED]
  Running Pointer_Arithmetic7/test.desc  [FAILED]
  Running Pointer_Arithmetic8/test.desc  [OK]
  Running Pointer_Arithmetic9/test.desc  [FAILED]
  Running Pointer_Assume1/test.desc  [SKIPPED]
  Running Pointer_array1/test.desc  [FAILED]
  Running Pointer_array2/test.desc  [FAILED]
  Running Pointer_array3/test.desc  [FAILED]
  Running Pointer_array4/test.desc  [FAILED]
  Running Pointer_array5/test.desc  [FAILED]
  Running Pointer_array6/test.desc  [FAILED]
  Running Pointer_byte_extract1/test.desc  [FAILED]
  Running Pointer_byte_extract2/test.desc  [FAILED]
  Running Pointer_byte_extract3/test.desc  [FAILED]
  Running Pointer_byte_extract4/test.desc  [FAILED]
  Running Pointer_byte_extract5/test.desc  [FAILED]
  Running Pointer_byte_extract6/test.desc  [FAILED]
  Running Pointer_byte_extract7/test.desc  [FAILED]
  Running Pointer_byte_extract8/test.desc  [SKIPPED]
  Running Pointer_byte_extract9/test.desc  [FAILED]
  Running Pointer_difference1/test.desc  [FAILED]
  Running Promotion1/test.desc  [FAILED]
  Running Promotion2/test.desc  [FAILED]
  Running Promotion3/test.desc  [FAILED]
  Running Quantifiers-assertion/test.desc  [OK]
  Running Quantifiers-assignment/test.desc  [OK]
  Running Quantifiers-copy/test.desc  [OK]
  Running Quantifiers-if/test.desc  [OK]
  Running Quantifiers-initialisation/test.desc  [OK]
  Running Quantifiers-initialisation2/test.desc  [OK]
  Running Quantifiers-invalid-var-range/test.desc  [OK]
  Running Quantifiers-not/test.desc  [OK]
  Running Quantifiers-not-exists/test.desc  [OK]
  Running Quantifiers-two-dimension-array/test.desc  [OK]
  Running Quantifiers-type/test.desc  [OK]
  Running Quantifiers1/test.desc  [FAILED]
  Running Recursion1/test.desc  [FAILED]
  Running Recursion2/test.desc  [FAILED]
  Running Recursion3/test.desc  [FAILED]
  Running Recursion4/test.desc  [FAILED]
  Running Recursion5/test.desc  [FAILED]
  Running Recursion6/test.desc  [FAILED]
  Running Sideeffects1/test.desc  [FAILED]
  Running Sideeffects2/test.desc  [FAILED]
  Running Sideeffects3/test.desc  [FAILED]
  Running Sideeffects4/test.desc  [FAILED]
  Running Sideeffects5/test.desc  [FAILED]
  Running Sideeffects6/test.desc  [FAILED]
  Running Static2/test.desc  [FAILED]
  Running Static_Functions1/test.desc  [FAILED]
  Running String1/test.desc  [FAILED]
  Running String2/test.desc  [FAILED]
  Running String3/test.desc  [SKIPPED]
  Running String4/test.desc  [FAILED]
  Running String5/test.desc  [FAILED]
  Running String6/test.desc  [FAILED]
  Running String7/test.desc  [FAILED]
  Running String_Literal1/test.desc  [FAILED]
  Running Struct_Bytewise1/test.desc  [FAILED]
  Running Struct_Bytewise2/test.desc  [FAILED]
  Running Struct_Initialization1/test.desc  [FAILED]
  Running Struct_Initialization10/test.desc  [FAILED]
  Running Struct_Initialization2/test.desc  [FAILED]
  Running Struct_Initialization3/test.desc  [FAILED]
  Running Struct_Initialization4/test.desc  [FAILED]
  Running Struct_Initialization5/test.desc  [FAILED]
  Running Struct_Initialization6/test.desc  [FAILED]
  Running Struct_Initialization7/test.desc  [FAILED]
  Running Struct_Initialization8/test.desc  [SKIPPED]
  Running Struct_Initialization9/test.desc  [FAILED]
  Running Struct_Padding1/test.desc  [FAILED]
  Running Typecast1/test.desc  [FAILED]
  Running Typecast2/test.desc  [FAILED]
  Running Undefined_Function1/test.desc  [OK]
  Running Undefined_Function2/test.desc  [OK]
  Running Union_Initialization1/test.desc  [FAILED]
  Running Unwinding_Assertions_Improved1/test.desc  [SKIPPED]
  Running Unwinding_Locality1/test.desc  [FAILED]
  Running Variadic1/test.desc  [SKIPPED]
  Running Visual_Studio_Types1/test.desc  [FAILED]
  Running Visual_Studio_Types2/test.desc  [FAILED]
  Running Volatile1/test.desc  [SKIPPED]
  Running Zero_Initialization1/test.desc  [FAILED]
  Running __func__1/test.desc  [FAILED]
  Running abs1/test.desc  [FAILED]
  Running address_space_size_limit1/test.desc  [OK]
  Running argv1/test.desc  [FAILED]
  Running array-tests/test.desc  [FAILED]
  Running atomic_section_seq1/test.desc  [FAILED]
  Running big-endian-array1/test.desc  [FAILED]
  Running byte_update1/test.desc  [FAILED]
  Running byte_update2/test.desc  [FAILED]
  Running byte_update3/test.desc  [FAILED]
  Running byte_update4/test.desc  [FAILED]
  Running byte_update5/test.desc  [FAILED]
  Running byte_update6/test.desc  [FAILED]
  Running byte_update7/test.desc  [FAILED]
  Running c99_Bool/test.desc  [FAILED]
  Running char1/test.desc  [FAILED]
  Running character_handling1/test.desc  [FAILED]
  Running comma1/test.desc  [FAILED]
  Running complex1/test.desc  [FAILED]
  Running compound_literal1/test.desc  [FAILED]
  Running const_ptr1/test.desc  [FAILED]
  Running constant_folding1/test.desc  [FAILED]
  Running constant_folding2/test.desc  [SKIPPED]
  Running divide-by-one-simplify/test.desc  [FAILED]
  Running enum1/test.desc  [FAILED]
  Running enum2/test.desc  [FAILED]
  Running enum3/test.desc  [FAILED]
  Running enum4/test.desc  [FAILED]
  Running enum5/test.desc  [FAILED]
  Running equality_through_array1/test.desc  [FAILED]
  Running equality_through_array2/test.desc  [FAILED]
  Running equality_through_array3/test.desc  [FAILED]
  Running equality_through_array4/test.desc  [FAILED]
  Running equality_through_array5/test.desc  [FAILED]
  Running equality_through_array6/test.desc  [FAILED]
  Running equality_through_array_of_struct1/test.desc  [FAILED]
  Running equality_through_array_of_struct2/test.desc  [FAILED]
  Running equality_through_array_of_struct3/test.desc  [FAILED]
  Running equality_through_array_of_struct4/test.desc  [FAILED]
  Running equality_through_struct1/test.desc  [FAILED]
  Running equality_through_struct2/test.desc  [FAILED]
  Running equality_through_struct3/test.desc  [FAILED]
  Running equality_through_struct4/test.desc  [FAILED]
  Running equality_through_struct5/test.desc  [FAILED]
  Running equality_through_struct_containing_arrays1/test.desc  [FAILED]
  Running equality_through_struct_containing_arrays2/test.desc  [FAILED]
  Running equality_through_struct_containing_arrays3/test.desc  [FAILED]
  Running equality_through_union1/test.desc  [FAILED]
  Running equality_through_union2/test.desc  [FAILED]
  Running equality_through_union3/test.desc  [FAILED]
  Running exit1/test.desc  [FAILED]
  Running extern_initialization1/test.desc  [FAILED]
  Running extern_initialization2/test.desc  [FAILED]
  Running for-break1/test.desc  [FAILED]
  Running for1/test.desc  [FAILED]
  Running for2/test.desc  [FAILED]
  Running for3/test.desc  [FAILED]
  Running function_option1/test.desc  [FAILED]
  Running gcc_attribute_alias1/test.desc  [FAILED]
  Running gcc_c99-bool-1/test.desc  [FAILED]
  Running gcc_conditional_expr1/test.desc  [FAILED]
  Running gcc_local_label1/test.desc  [FAILED]
  Running gcc_statement_expression1/test.desc  [FAILED]
  Running gcc_statement_expression2/test.desc  [FAILED]
  Running gcc_statement_expression3/test.desc  [FAILED]
  Running gcc_statement_expression4/test.desc  [FAILED]
  Running gcc_statement_expression5/test.desc  [FAILED]
  Running gcc_vector1/test.desc  [FAILED]
  Running gcc_vector2/test.desc  [FAILED]
  Running getenv-overflow1/test.desc  [FAILED]
  Running goto1/test.desc  [FAILED]
  Running goto2/test.desc  [FAILED]
  Running goto3/test.desc  [FAILED]
  Running goto4/test.desc  [FAILED]
  Running graphml_witness1/test.desc  [FAILED]
  Running guard1/test.desc  [FAILED]
  Running if1/test.desc  [FAILED]
  Running if2/test.desc  [FAILED]
  Running if3/test.desc  [FAILED]
  Running if4/test.desc  [FAILED]
  Running inequality-with-constant-normalisation/test.desc  [FAILED]
  Running inline1/test.desc  [FAILED]
  Running int-to-float1/test.desc  [FAILED]
  Running int-to-float2/test.desc  [FAILED]
  Running locations1/test.desc  [FAILED]
  Running noop1/test.desc  [FAILED]
  Running null1/test.desc  [FAILED]
  Running null2/test.desc  [FAILED]
  Running null3/test.desc  [FAILED]
  Running offsetof1/test.desc  [FAILED]
  Running pipe1/test.desc  [FAILED]
  Running realloc1/test.desc  [FAILED]
  Running realloc2/test.desc  [FAILED]
  Running realloc3/test.desc  [FAILED]
  Running return1/test.desc  [FAILED]
  Running return3/test.desc  [FAILED]
  Running return4/test.desc  [FAILED]
  Running return5/test.desc  [FAILED]
  Running scanf1/test.desc  [FAILED]
  Running simplify-full-test/test.desc  [FAILED]
  Running simplify-function-call-array-element-pointer/test.desc  [FAILED]
  Running simplify-function-call-array-pointer/test.desc  [FAILED]
  Running simplify-function-call-pointer-access/test.desc  [FAILED]
  Running simplify-global-array-access/test.desc  [FAILED]
  Running simplify-local-array-access/test.desc  [FAILED]
  Running simplify-pointer-access/test.desc  [FAILED]
  Running strchr1/test.desc  [FAILED]
  Running strtol1/test.desc  [FAILED]
  Running strtol2/test.desc  [FAILED]
  Running struct1/test.desc  [FAILED]
  Running struct3/test.desc  [FAILED]
  Running struct4/test.desc  [FAILED]
  Running struct6/test.desc  [FAILED]
  Running struct7/test.desc  [FAILED]
  Running struct8/test.desc  [FAILED]
  Running struct9/test.desc  [FAILED]
  Running switch1/test.desc  [FAILED]
  Running switch2/test.desc  [FAILED]
  Running switch3/test.desc  [FAILED]
  Running switch4/test.desc  [FAILED]
  Running switch5/test.desc  [FAILED]
  Running switch6/test.desc  [FAILED]
  Running union1/test.desc  [SKIPPED]
  Running union2/test.desc  [FAILED]
  Running union3/test.desc  [FAILED]
  Running union4/test.desc  [FAILED]
  Running union5/test.desc  [FAILED]
  Running union6/test.desc  [FAILED]
  Running union7/test.desc  [FAILED]
  Running union8/test.desc  [FAILED]
  Running unsigned___int128/test.desc  [FAILED]
  Running unsigned_char1/test.desc  [FAILED]
  Running va_list1/test.desc  [FAILED]
  Running va_list2/test.desc  [SKIPPED]
  Running variable-access-to-constant-array/test.desc  [FAILED]
  Running void_ifthenelse/test.desc  [FAILED]
  Running while1/test.desc  [FAILED]

Tests failed
  375 of 414 tests failed, 20 tests skipped

cbmc-cover

Running tests
  Running assertion1/test.desc  [FAILED]
  Running branch1/test.desc  [FAILED]
  Running branch2/test.desc  [FAILED]
  Running branch3/test.desc  [FAILED]
  Running branch4/test.desc  [FAILED]
  Running condition1/test.desc  [FAILED]
  Running cover1/test.desc  [FAILED]
  Running decision1/test.desc  [FAILED]
  Running inlining1/test.desc  [FAILED]
  Running location1/test.desc  [FAILED]
  Running location11/test.desc  [FAILED]
  Running location12/test.desc  [FAILED]
  Running location13/test.desc  [FAILED]
  Running location14/test.desc  [FAILED]
  Running location15/test.desc  [SKIPPED]
  Running location16/test.desc  [FAILED]
  Running mcdc1/test.desc  [FAILED]
  Running mcdc10/test.desc  [FAILED]
  Running mcdc11/test.desc  [FAILED]
  Running mcdc12/test.desc  [FAILED]
  Running mcdc13/test.desc  [FAILED]
  Running mcdc14/test.desc  [FAILED]
  Running mcdc2/test.desc  [FAILED]
  Running mcdc3/test.desc  [FAILED]
  Running mcdc4/test.desc  [FAILED]
  Running mcdc5/test.desc  [FAILED]
  Running mcdc6/test.desc  [FAILED]
  Running mcdc7/test.desc  [FAILED]
  Running mcdc8/test.desc  [FAILED]
  Running mcdc9/test.desc  [FAILED]

Tests failed
  29 of 30 tests failed, 1 test skipped

cpp

Running tests
  Running Address_of_Method2/test.desc  [OK]
  Running Address_of_Method3/test.desc  [OK]
  Running Apple_extensions1/test.desc  [OK]
  Running Bit_fields1/test.desc  [SKIPPED]
  Running Constant1/test.desc  [OK]
  Running Constant2/test.desc  [OK]
  Running Constant3/test.desc  [OK]
  Running Constant4/test.desc  [OK]
  Running Decltype1/test.desc  [OK]
  Running Decltype2/test.desc  [OK]
  Running Decltype3/test.desc  [SKIPPED]
  Running Friend2/test.desc  [OK]
  Running Function_Bodies1/test.desc  [OK]
  Running Function_Overloading1/test.desc  [OK]
  Running Function_Overloading2/test.desc  [SKIPPED]
  Running List_initialization1/test.desc  [SKIPPED]
  Running Method_Scope1/test.desc  [OK]
  Running Method_qualifier1/test.desc  [OK]
  Running ModeC1/test.desc  [OK]
  Running ModeC2/test.desc  [OK]
  Running ModeC3/test.desc  [FAILED]
  Running Pointer_Conversion1/test.desc  [OK]
  Running Pointer_Conversion2/test.desc  [OK]
  Running Qualifiers_In_Template_Specialisation1/test.desc  [SKIPPED]
  Running Resolver1/test.desc  [OK]
  Running Resolver10/test.desc  [OK]
  Running Resolver11/test.desc  [OK]
  Running Resolver12/test.desc  [OK]
  Running Resolver2/test.desc  [OK]
  Running Resolver3/test.desc  [OK]
  Running Resolver4/test.desc  [OK]
  Running Scope1/test.desc  [OK]
  Running Template_Default_Parameters1/test.desc  [OK]
  Running Template_Instantiation1/test.desc  [OK]
  Running Template_Instantiation2/test.desc  [SKIPPED]
  Running Template_Instantiation3/test.desc  [SKIPPED]
  Running Template_Instantiation4/test.desc  [SKIPPED]
  Running Template_Instantiation5/test.desc  [SKIPPED]
  Running Template_Parameters1/test.desc  [OK]
  Running Template_Specialisation1/test.desc  [OK]
  Running Template_Specialisation2/test.desc  [SKIPPED]
  Running Templates1/test.desc  [OK]
  Running Templates2/test.desc  [OK]
  Running Templates7/test.desc  [OK]
  Running Trailing_Return_Type1/test.desc  [OK]
  Running Unary_Function_Overload1/test.desc  [SKIPPED]
  Running Unary_Function_Overload2/test.desc  [SKIPPED]
  Running Unary_Function_Overload3/test.desc  [SKIPPED]
  Running Unary_Function_Overload4/test.desc  [OK]
  Running Union_Constructor/test.desc  [OK]
  Running auto1/test.desc  [SKIPPED]
  Running bitwise_and1/test.desc  [OK]
  Running bool1/test.desc  [OK]
  Running constexpr1/test.desc  [SKIPPED]
  Running enum1/test.desc  [SKIPPED]
  Running enum2/test.desc  [OK]
  Running enum3/test.desc  [SKIPPED]
  Running enum4/test.desc  [OK]
  Running enum5/test.desc  [SKIPPED]
  Running enum6/test.desc  [OK]
  Running enum7/test.desc  [OK]
  Running enum8/test.desc  [OK]
  Running enum_class1/test.desc  [SKIPPED]
  Running lvalue1/test.desc  [OK]
  Running namespace4/test.desc  [OK]
  Running nullptr1/test.desc  [OK]
  Running reinterpret_cast1/test.desc  [OK]
  Running sizeof1/test.desc  [OK]
  Running sizeof2/test.desc  [OK]
  Running sizeof3/test.desc  [OK]
  Running static_assert1/test.desc  [OK]
  Running switch1/test.desc  [OK]
  Running type_traits1/test.desc  [SKIPPED]
  Running type_traits_essentials1/test.desc  [SKIPPED]
  Running typecast_ambiguity1/test.desc  [OK]
  Running typecast_ambiguity2/test.desc  [OK]
  Running typedef1/test.desc  [OK]
  Running typedef2/test.desc  [OK]
  Running union3/test.desc  [OK]
  Running union4/test.desc  [OK]
  Running union5/test.desc  [OK]
  Running virtual1/test.desc  [SKIPPED]
  Running windows_h_VS_2005/test.desc  [OK]
  Running windows_h_VS_2008/test.desc  [OK]
  Running windows_h_VS_2010/test.desc  [OK]
  Running windows_h_VS_2012/test.desc  [OK]

Tests failed
  1 of 86 tests failed, 22 tests skipped

goto-analyzer

Running tests
  Running intervals1/test.desc  [FAILED]
  Running intervals2/test.desc  [SKIPPED]
  Running intervals3/test.desc  [FAILED]
  Running intervals4/test.desc  [SKIPPED]
  Running intervals5/test.desc  [FAILED]
  Running intervals6/test.desc  [FAILED]
  Running intervals7/test.desc  [FAILED]

Tests failed
  5 of 7 tests failed, 2 tests skipped

goto-instrument

Running tests
  Running argc-argv1/test.desc  [FAILED]
  Running const-struct1/test.desc  [FAILED]
  Running const-struct2/test.desc  [FAILED]
  Running const-struct3/test.desc  [FAILED]
  Running const-union1/test.desc  [FAILED]
  Running data-flow1/test.desc  [FAILED]
  Running dependence-graph1/test.desc  [FAILED]
  Running inline_01/test.desc  [FAILED]
  Running inline_02/test.desc  [FAILED]
  Running inline_03/test.desc  [FAILED]
  Running inline_04/test.desc  [FAILED]
  Running inline_05/test.desc  [FAILED]
  Running inline_06/test.desc  [FAILED]
  Running inline_07/test.desc  [FAILED]
  Running inline_08/test.desc  [FAILED]
  Running inline_09/test.desc  [FAILED]
  Running inline_10/test.desc  [FAILED]
  Running inline_11/test.desc  [FAILED]
  Running inline_12/test.desc  [FAILED]
  Running is-threaded1/test.desc  [FAILED]
  Running restore-returns1/test.desc  [FAILED]
  Running restore-returns2/test.desc  [FAILED]
  Running slice-global-inits1/test.desc  [FAILED]
  Running slice01/test.desc  [SKIPPED]
  Running slice02/test.desc  [SKIPPED]
  Running slice03/test.desc  [FAILED]
  Running slice04/test.desc  [FAILED]
  Running slice05/test.desc  [FAILED]
  Running slice06/test.desc  [FAILED]
  Running slice07/test.desc  [SKIPPED]
  Running slice08/test.desc  [FAILED]
  Running slice09/test.desc  [FAILED]
  Running slice10/test.desc  [FAILED]
  Running slice11/test.desc  [FAILED]
  Running slice12/test.desc  [FAILED]
  Running slice13/test.desc  [SKIPPED]
  Running slice14/test.desc  [SKIPPED]
  Running slice15/test.desc  [FAILED]
  Running slice16/test.desc  [FAILED]
  Running slice17/test.desc  [SKIPPED]
  Running slice18/test.desc  [SKIPPED]
  Running slice19/test.desc  [SKIPPED]
  Running slice20/test.desc  [SKIPPED]
  Running slice21/test.desc  [SKIPPED]
  Running unwind-assert1/test.desc  [FAILED]
  Running unwind-assert2/test.desc  [FAILED]
  Running unwind-assert3/test.desc  [FAILED]
  Running unwind-assume1/test.desc  [FAILED]
  Running unwind-assume2/test.desc  [FAILED]
  Running unwind-break-loop1/test.desc  [FAILED]
  Running unwind-break-loop2/test.desc  [FAILED]
  Running unwind-continue-as-loops1/test.desc  [FAILED]
  Running unwind-continue-loop1/test.desc  [FAILED]
  Running unwind-continue-loop2/test.desc  [FAILED]
  Running unwind-do-while-loop1/test.desc  [FAILED]
  Running unwind-do-while-loop2/test.desc  [FAILED]
  Running unwind-empty-loop1/test.desc  [FAILED]
  Running unwind-empty-loop2/test.desc  [FAILED]
  Running unwind-nested-loops1/test.desc  [FAILED]
  Running unwind-nested-loops2/test.desc  [FAILED]
  Running unwind-simple-loop1/test.desc  [FAILED]
  Running unwind-simple-loop2/test.desc  [FAILED]
  Running unwind-unwind-log1/test.desc  [FAILED]
  Running unwind-unwindset-file1/test.desc  [FAILED]
  Running unwind-unwindset1/test.desc  [FAILED]
  Running unwind-unwindset2/test.desc  [FAILED]
  Running unwind-unwindset3/test.desc  [FAILED]
  Running unwind-unwindset4/test.desc  [FAILED]
  Running unwind-unwindset5/test.desc  [FAILED]
  Running unwind-zero-unwind1/test.desc  [FAILED]
  Running unwind-zero-unwind2/test.desc  [FAILED]
  Running unwind-zero-unwind3/test.desc  [FAILED]
  Running volatile-struct1/test.desc  [FAILED]

Tests failed
  63 of 73 tests failed, 10 tests skipped

k-induction

Running tests
  Running basic1/test.desc  [OK]
  Running basic2/test.desc  [OK]
  Running basic3/test.desc  [OK]
  Running basic4/test.desc  [OK]

All tests were successful

[tautschnig]

So line 113 is data=new dt(*old_data); - I suppose an "indirect leak" is meant to say that we are replacing a pointer to an allocation by a new allocation, thus (seemingly) rendering the previous allocation a leak. Yet the claim here is that through reference counting we will make sure there exists at least one more pointer to that original allocation.

[mgudemann]

yes, this may very well be a false alarm - I'll see whether one can ignore this in the analysis and re-run.

[mgudemann]

ok, I did not get any direct leak when running an instrumented CBMC using ASAN_OPTIONS="halt_on_error=false" on either the regression tests or one of the Java benchmarks.
All reported errors seem to be of the above type