Skip to content

indirect leak in irept::detach #569

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
mgudemann opened this issue Feb 22, 2017 · 6 comments
Closed

indirect leak in irept::detach #569

mgudemann opened this issue Feb 22, 2017 · 6 comments

Comments

@mgudemann
Copy link
Contributor

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
Copy link
Collaborator

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

@mgudemann
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link
Collaborator

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
Copy link
Contributor Author

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

@mgudemann
Copy link
Contributor Author

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

@mgudemann mgudemann mentioned this issue Mar 23, 2017
Closed
This was referenced Apr 14, 2017
Merged
Open
NathanJPhillips pushed a commit to NathanJPhillips/cbmc that referenced this issue Aug 22, 2018
@smowton
Squashed 'benchmarks/LIBRARIES/models/' changes from 1e8b77c83..24023…
54a95ff 
…6357

240236357 Merge pull request diffblue#581 from diffblue/forejtv/simpler-file
8ef53a50a simplified constructor for java.io.File
d1c08d982 Put non-simple File.java into simple models
13c22a856 Merge pull request diffblue#578 from diffblue/jeannie/UpdateDTUversion
39202a4e5 Merge pull request diffblue#577 from diffblue/allredj/complete-linked-list-documentation
2d94c7b47 Update deeptest-utils version.
ab300bbe2 Complete documentation of LinkedList
4f77b90dd Merge pull request diffblue#544 from diffblue/collections-reverse
e78b7f02c Tests for Collections model
137622bcf Model for java/util/Collections
422197c51 Added java/util/Collections
33c1410b9 Merge pull request diffblue#576 from diffblue/smowton/admin/increase-to-depth-1600
85000a8ac Bump depth to 1600
927fef36d Merge pull request diffblue#571 from diffblue/zgoriely/linked-list-basic
8621e0d71 Addressing reviewer comments
46376144c Add tests for LinkedList methods
e4782ab96 Implement model for remaining basic LinkedList methods
0a32c4de5 Merge pull request diffblue#566 from diffblue/zgoriely/linked-list
7cc397a82 Add tests for new methods
e86ade7cb Implement methods for LinkedList
6fe84d51a Merge pull request diffblue#569 from diffblue/allredj/update-dtu-131
7bf5a1a80 Update DeepTestUtils to 1.3.1
9df72dd93 Merge pull request diffblue#560 from diffblue/zgoriely/arrays-simple-equals
78228133b Re-enable tests depending on Arrays.equals
b011e0cf5 Add Tests for Simple Arrays.equals
1a76bd166 Implement Simple Model for Arrays.equals
4d14a9a57 Merge pull request diffblue#543 from diffblue/linked-list-add-all
27c9f5da6 Merge pull request diffblue#562 from diffblue/zgoriely/arrays-equals-fix
b19e50c71 Tests for LinkedList init(c)|addAll(c)
394db6890 Modelled java/util/LinkedList.(<init>(Collection)|addAll)
950aae85c Merge pull request diffblue#565 from diffblue/zgoriely/hashset-fix
534a85708 Arrays Equals Model fix - Double and Float
74fa617b8 Fixing HashSet.addAll method
dac4774ce Merge pull request diffblue#542 from diffblue/java-util-optional
396f52c45 Tests for Optional model
d11e8faed Tidying Optional Model
3f8e7e19f Modelled java/util/Optional and java/util/function/(Supplier|Consumer)
8db4ad90e Emptied java/util/Optional and java/util/function/(Supplier|Consumer)
4c3781871 Added java/util/Optional and java/util/function/(Supplier|Consumer)
a6cbe0c51 Merge pull request diffblue#564 from diffblue/zgoriely/arrays-comparator-fix
ab7638920 Fix for Comparator sort test-gen failure
13218fec0 Merge pull request diffblue#545 from diffblue/arrays-sort
bd27eeac1 Fixing up tags in Base64 Models
14f7cda29 Tests for Arrays.sort
8c4c1c524 Model java/util/Arrays.sort
edefabb77 Empty java/util/Comparator
5c39ba9e2 Add java/util/Comparator
941eefa80 Merge pull request diffblue#563 from diffblue/allredj/travis-housekeeping
996c4aab8 Travis: Don't save html report
37640904c Travis: install gauge html-report
72330e6ce Linting
3a97f9fa5 Travis: Remove unneeded addon installs
c6d77308b Merge pull request diffblue#556 from diffblue/allredj/update-modeltests-gitignore
11409e1aa Merge pull request diffblue#375 from diffblue/jeannie/setTimeZoneAndOthers
6b4808330 Update .class files
7deac9024 Tag all failing tests with appropriate ticket no.
c832fba9b Mock Calendar and fix some things in the model
726558344 Re-enable fastTime field in Date model
e5f994525 Updates CProver.nondet methods for not modelled functions.
d43a366cf Updates documentation in javadocs for java.util.Date
e65c0f6aa Tests java.text.SimpleDateFormat
798fd0b5e Models java.text.SimpleDateFormat
0499abc91 Models java.text.DateFormat getTimeZone() and setTimeZone()
6d96405f7 Marks all methods as notModelled() in Format classes
477fcc92d Initial commit for java.text.Format, DateFormat and SimpleDateFormat models.
efd6fe8e3 Tests java.util.GregorianCalendar
e4e0d40ff Tests java.util.Calendar
b87c250f8 Models java.util.GregorianCalendar()
e03f25170 Marks all methods as notModelled() for java.util.GregorianCalendar
ce2549199 Initial commit for java.util.GregorianCalendar
9d85399fa Models java.util.Calendar
d0d31e9ed Marks all methods as notModelled() in java.util.Calendar
71d877078 Initial commit for java.util.Calendar
149aa4da6 Models ZoneInfo getRawOffset() and uses it for getOffset()
8d9a9ac67 Merge pull request diffblue#561 from diffblue/zgoriely/model-test-generator-improvement
0a7e92e0d Fixing a couple bugs in model test generator
7ce6d62a9 Merge pull request diffblue#558 from diffblue/antonia/appendable-annotation
562ffb424 Merge pull request diffblue#559 from diffblue/antonia/enable-TG-3905-tests
e32331aa9 Merge pull request diffblue#555 from diffblue/zgoriely/arrays-fill
4d1111fa6 Enable tests for TG-3905
fb5308932 Move Appendable test to appropriate folder
2149e3ad8 Pick StringBuilder as an Appendable implementation
9b2a4a30a Arrays fill model
1fcddca3f Merge pull request diffblue#557 from diffblue/zgoriely/arrays-equals
0ef93d6dd Updated test class names and test method names
c037628e6 Re-Enabling tests that rely on Arrays.equals
8329b761d Merge pull request diffblue#541 from diffblue/emptier-script
bc31d0bdf Merge pull request diffblue#551 from diffblue/zgoriely/arrays-equals
f9f914b8f Update modelTests .gitignore
8469f6c28 Tests for Arrays.equals methods
2eef3d595 Model for Arrays.equals methods
bf7b6f191 Merge pull request diffblue#550 from diffblue/cesaro/java-sync-fix
1a93b39d5 Re-enable tests in PushbackReader.spec, see e21b471
dd8689737 Merge pull request diffblue#547 from diffblue/svorenova/enable_tests_tg3514
5fd67cde8 Use Gauge tear-down steps
e1b2b5241 Update ticket number for disabled tests for mocking with inheritance
9ee355cd5 Merge pull request diffblue#554 from diffblue/allredj/travis-use-obfuscated-build
5fee9930a Use obfuscated test-gen build in models-library
7502e471d Merge pull request diffblue#540 from diffblue/java-concurrency-synchronization-models
e21b471ab Temporary disabled a number of tests in 'PushbackReader.spec'
7f1eb804d Emptier script
d0b941b83 Changes to support PR cbmc#2280
5915ce44d Merge pull request diffblue#536 from diffblue/antonia/unnecessary-gauge-steps
e8b4888f9 Merge pull request diffblue#538 from diffblue/bugfix/TG-1888/put-tests-in-appropriate-packages
8fd5af6eb Tidy up Verify steps in spec files
da8b4ac38 Don't use java or javax packages
4ec167eec Adding test for checking getPackageFromMethod
91ea20ce3 Put tests in to the package that the function under test is in
6e6b59698 Merge pull request diffblue#533 from diffblue/allredj/testrunner-start-with-unwind-2
57b73a8b0 Merge pull request diffblue#504 from diffblue/forejtv/simple-base64
8907ffd20 Simplified model for Base64
8d521d65d Skip some tests that fail due to TG-3981
35621a7e9 Merge pull request diffblue#530 from diffblue/romain/string-init-charset
efebf5cec Use CProverString.substring
d929a005f Use a reversible version of getBytes
c1e020c3d Add test for constructor from byte[] and charset
07004ec1b Model for String constructor from byte[], charset
136326682 Use equality on name for charsets
e45df98d0 Use CProverString.equals instead of ==
61c713714 Define a CProverString.equals function
c0ef4fe7d Merge pull request diffblue#519 from diffblue/allredj/linkedhashset
338a1cdfc Merge pull request diffblue#528 from diffblue/allredj/simple-linkedhashset
cf1f27e96 Added original model for Base64
8676ea6b5 Merge pull request diffblue#535 from diffblue/antonia/stringreader-optimisations
0f051858c Tests for LinkedHashSet (simple model)
d964fa763 Make HashSet fields package-private (simple model)
beaf7d1bf Simple model for LinkedHashSet
01e2b787c Import LinkedHashSet.java from JDK
400db2ba0 Add missing Diffblue Javadoc tags
f50914877 Use more efficient charAt in StringReader
6a60301b0 Clarify differences from JDK StringReader
c95f30f27 Load a StringReader when loading PushbackReader
8290e5b13 Start generating tests with unwind 2
8861b24f1 Tests for LinkedHashSet
81ca53b05 Model for LinkedHashSet
5d9420c1d Import LinkedHashSet.java from JDK
4e22d539b TestRunner: Factor out debug output
9616e1769 Merge pull request diffblue#531 from diffblue/romain/nondet-initialize-file
8553bf0e5 Activate cproverNondetInitialize for file
c0d1c05dc Merge pull request diffblue#532 from diffblue/allredj/fix-stringbuffer-append
71e3b0788 Merge pull request diffblue#534 from diffblue/allredj/use-fornotmodelled-in-simple-models-2
c0f10640b Merge pull request #529 from diffblue/jeannie/TestRunnerImportsUpdate
65b68beeb Merge pull request diffblue#516 from diffblue/allredj/exhibit-mocking-bug-with-inheritance
2588b96c0 Use appropriate header for tests.
fc3f1c53a Use short name for annotation in TestRunner.
0e9da3a50 Avoid using nondet statements where possible
a20e778b4 Build modelling utils with "package"
753eea477 Copy over cprover package from standard models
67199cdb2 Fix StringBuffer.append
3f2ac3406 Disable tests that suffer from TG-3514
d2dabe327 Make tests sensitive to mocking problems
532d146f3 Merge pull request diffblue#515 from diffblue/antonia/implement-annotation
0048a020c Add tests for classes given in annotations
2e6182b10 Annotate common abstract classes
39f6d72f4 Add java.lang.Appendable interface
bc383f3b2 Add java.io.Flushable interface
83dffab13 Add java.lang.AutoCloseable interface
18bd2e55b Add java.io.Closeable interface
f37ca90df Add java.lang.Readable interface
a8369c332 Add implementation annotation to simple models
d06449814 Show "Preferred..." annotations in Javadoc

git-subtree-dir: benchmarks/LIBRARIES/models
git-subtree-split: 240236357fc9fb1cb87bf5adacaa1b27786ff84b
NathanJPhillips pushed a commit to NathanJPhillips/cbmc that referenced this issue Sep 6, 2018
Merge pull request diffblue#569 from diffblue/webgoat-demo-working-br…
8e5f83e 
…anch

[SEC-638] [SEC-639] Webgoat demo working branch
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@tautschnig @mgudemann