diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
842 stars 262 forks source link

Memory leak with full rt.jar, lazy-methods #877

Open reuk opened 7 years ago

reuk commented 7 years ago

I'm not sure if this is the minimal test case, but I think it's pretty close. On f5aa612 (tip of test-gen-support), the following test case results in a memory leak.

package Iterator;

import java.util.Iterator;
import org.cprover.CProver;

class MyIterator implements Iterator {
  private int index = 0;

  public boolean hasNext() {
    return index < 5;
  }

  public Object next() {
    index += 1;
    return null;
  }
}

public class Loop_foreach_Pass {
  public static void main(String[] args) {
    int iterations = 0;

    Iterator iterator = new MyIterator();
    while (iterator.hasNext()) {
      iterator.next();
      iterations += 1;
    }

    assert iterations == 5;
  }
}

command-line:

cbmc Iterator/Loop_foreach_Pass.class --lazy-methods --classpath ../build/linux-x86_64-normal-server-release/images/j2re-image/lib/rt.jar:. --unwind 8

truncated output:

** 0 of 151 failed (1 iteration)
VERIFICATION SUCCESSFUL

=================================================================
==17043==ERROR: LeakSanitizer: detected memory leaks

Indirect leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x14a6a89 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:109:3
    #6 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #7 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #8 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)/home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #9 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #10 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #11 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #12 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #13 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #14 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #15 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x14c60b1 in struct_union_typet::set_tag(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:263:39
    #6 0x14a693a in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:108:3
    #7 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #8 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #9 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)/home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #10 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #11 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #12 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #13 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #14 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #15 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #16 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0x5ad637 in exprt::type() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:59:47
    #6 0x2c9af6e in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:999:10
    #7 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #8 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #9 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #10 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #11 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #12 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #13 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #14 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #15 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #16 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #17 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #18 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #19 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #20 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #21 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #22 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #23 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0x5ad637 in exprt::type() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:59:47
    #6 0x2c97efc in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:12
    #7 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #8 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #9 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #10 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #11 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #12 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #13 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #14 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #15 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #16 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #17 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #18 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #19 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #20 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #21 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #22 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #23 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0x5ad637 in exprt::type() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:59:47
    #6 0x2c9af6e in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:999:10
    #7 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #8 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #9 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #10 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #11 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #12 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #13 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #14 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #15 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #16 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #17 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #18 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #19 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #20 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #21 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #22 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x14a90f5 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:142:3
    #6 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #7 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #8 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)/home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #9 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #10 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #11 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #12 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #13 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #14 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #15 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0x5ad637 in exprt::type() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:59:47
    #6 0x2c9af6e in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:999:10
    #7 0x2c9b968 in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:1002:9
    #8 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #9 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #10 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #11 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #12 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #13 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #14 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #15 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #16 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #17 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #18 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #19 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #20 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #21 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #22 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #23 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 256 byte(s) in 2 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0xbfa9ca in irept::set(dstringt const&, long long) /home/reuben/development/cbmc/src/util/irep.cpp:430:3
    #5 0x14c5ee5 in class_typet::class_typet() /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:338:5
    #6 0x14a6828 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:106:15
    #7 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #8 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #9 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)/home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #10 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #11 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #12 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #13 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #14 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #15 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #16 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 144 byte(s) in 3 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xc15d33 in __gnu_cxx::new_allocator<std::_Rb_tree_node<std::pair<dstringt const, irept> > >::allocate(unsigned long, void const*) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/ext/new_allocator.h:104:27
    #2 0xc15c83 in std::allocator_traits<std::allocator<std::_Rb_tree_node<std::pair<dstringt const, irept> > > >::allocate(std::allocator<std::_Rb_tree_node<std::pair<dstringt const, irept> > >&, unsigned long) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/alloc_traits.h:491:16
    #3 0xc158fc in std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_M_get_node() /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:491:16
    #4 0xc15694 in std::_Rb_tree_node<std::pair<dstringt const, irept> >* std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_M_create_node<std::pair<dstringt const, irept> const&>(std::pair<dstringt const, irept> const&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:545:23
    #5 0xc15544 in std::_Rb_tree_node<std::pair<dstringt const, irept> >* std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_Alloc_node::operator()<std::pair<dstringt const, irept> const&>(std::pair<dstringt const, irept> const&) const /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:459:13
    #6 0xc14c38 in std::_Rb_tree_node<std::pair<dstringt const, irept> >* std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_M_clone_node<std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_Alloc_node>(std::_Rb_tree_node<std::pair<dstringt const, irept> > const*, std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_Alloc_node&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:569:23
    #7 0xc14295 in std::_Rb_tree_node<std::pair<dstringt const, irept> >* std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_M_copy<std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_Alloc_node>(std::_Rb_tree_node<std::pair<dstringt const, irept> > const*, std::_Rb_tree_node<std::pair<dstringt const, irept> >*, std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_Alloc_node&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:1586:20
    #8 0xc12f19 in std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_M_copy(std::_Rb_tree_node<std::pair<dstringt const, irept> > const*, std::_Rb_tree_node<std::pair<dstringt const,irept> >*) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:783:9
    #9 0xc11e6b in std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::_Rb_tree(std::_Rb_tree<dstringt, std::pair<dstringt const, irept>, std::_Select1st<std::pair<dstringt const, irept> >, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > > const&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_tree.h:819:18
    #10 0xc10e6a in std::map<dstringt, irept, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > >::map(std::map<dstringt, irept, std::less<dstringt>, std::allocator<std::pair<dstringt const, irept> > > const&) /usr/bin/../lib/gcc/x86_64-linux-gnu/5.4.0/../../../../include/c++/5.4.0/bits/stl_map.h:186:9
    #11 0xc054c3 in irept::dt::dt(irept::dt const&) /home/reuben/development/cbmc/src/util/./irep.h:260:9
    #12 0xbf658e in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:14
    #13 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #14 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #15 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #16 0x5ad637 in exprt::type() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:59:47
    #17 0x2c9af6e in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:999:10
    #18 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #19 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #20 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #21 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #22 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #23 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #24 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #25 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #26 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #27 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #28 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #29 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x128a3b1 in symbol_typet::set_identifier(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:122:5
    #6 0x1288520 in symbol_typet::symbol_typet(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:117:5
    #7 0x14a88f6 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:133:18
    #8 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #9 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #10 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #11 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #12 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #13 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #14 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #15 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #16 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #17 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5dd5aa in typet::typet(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/type.h:24:39
    #6 0x5e011a in type_with_subtypet::type_with_subtypet(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/type.h:120:52
    #7 0xc8dc07 in bitvector_typet::bitvector_typet(dstringt const&, unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1033:5
    #8 0xc8d568 in signedbv_typet::signedbv_typet(unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1187:5
    #9 0x14676de in java_int_type() /home/reuben/development/cbmc/src/java_bytecode/java_types.cpp:33:10
    #10 0x146f852 in java_type_from_string(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_types.cpp:425:20
    #11 0x14abef9 in java_bytecode_convert_classt::convert(symbolt&, java_bytecode_parse_treet::fieldt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:244:20
    #12 0x14aa08c in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:158:5
    #13 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #14 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #15 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #16 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #17 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #18 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #19 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #20 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #21 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #22 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0xbfa9ca in irept::set(dstringt const&, long long) /home/reuben/development/cbmc/src/util/irep.cpp:430:3
    #5 0xb9594f in bitvector_typet::set_width(unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1045:5
    #6 0xc8dc5a in bitvector_typet::bitvector_typet(dstringt const&, unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1035:5
    #7 0x1473d18 in c_bool_typet::c_bool_typet(unsigned long) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:1441:5
    #8 0x146912e in java_boolean_type() /home/reuben/development/cbmc/src/java_bytecode/java_types.cpp:172:10
    #9 0x177911b in java_root_class(symbolt&) /home/reuben/development/cbmc/src/java_bytecode/java_root_class.cpp:37:22
    #10 0x14ab6f4 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:179:5
    #11 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #12 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #13 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #14 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #15 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #16 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #17 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #18 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #19 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #20 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5dd5aa in typet::typet(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/type.h:24:39
    #6 0x128847b in symbol_typet::symbol_typet(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:115:53
    #7 0x14a88f6 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:133:18
    #8 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #9 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #10 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #11 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #12 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #13 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #14 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #15 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #16 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #17 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x128acf1 in struct_union_typet::componentt::set_name(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:185:14
    #6 0x1778ef1 in java_root_class(symbolt&) /home/reuben/development/cbmc/src/java_bytecode/java_root_class.cpp:35:5
    #7 0x14ab6f4 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:179:5
    #8 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #9 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #10 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #11 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #12 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #13 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #14 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #15 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #16 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #17 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x1289d01 in struct_union_typet::componentt::set_pretty_name(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:215:14
    #6 0x14af3dc in java_bytecode_convert_classt::convert(symbolt&, java_bytecode_parse_treet::fieldt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:287:5
    #7 0x14aa08c in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:158:5
    #8 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #9 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #10 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #11 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #12 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #13 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #14 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #15 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #16 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #17 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0x5dd690 in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #6 0x167e551 in source_locationt::set_java_bytecode_index(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/source_location.h:134:5
    #7 0x165e2e8 in java_bytecode_parsert::rbytecode(std::vector<java_bytecode_parse_treet::instructiont, std::allocator<java_bytecode_parse_treet::instructiont> >&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:765:5
    #8 0x1668ae0 in java_bytecode_parsert::rmethod_attribute(java_bytecode_parse_treet::methodt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:995:5
    #9 0x167747c in java_bytecode_parsert::rmethod(java_bytecode_parse_treet::classt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1567:5
    #10 0x1655577 in java_bytecode_parsert::rmethods(java_bytecode_parse_treet::classt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1515:5
    #11 0x1646ca5 in java_bytecode_parsert::rClassFile() /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:314:3
    #12 0x1644041 in java_bytecode_parsert::parse() /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:219:5
    #13 0x1677b0a in java_bytecode_parse(std::istream&, java_bytecode_parse_treet&, message_handlert&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1591:22
    #14 0x1678e1b in java_bytecode_parse(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, java_bytecode_parse_treet&, message_handlert&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1625:10
    #15 0x129a324 in java_class_loadert::get_parse_tree(java_class_loader_limitt&, dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/java_class_loader.cpp:184:13
    #16 0x1294405 in java_class_loadert::operator()(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/java_class_loader.cpp:62:7
    #17 0x11f05ef in java_bytecode_languaget::parse(std::istream&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:205:5
    #18 0x2d8fad7 in language_uit::parse(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/langapi/language_ui.cpp:128:6
    #19 0x2d8d155 in language_uit::parse() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:74:8
    #20 0x10cfe84 in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:705:10
    #21 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #22 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #23 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #24 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0xbfa9ca in irept::set(dstringt const&, long long) /home/reuben/development/cbmc/src/util/irep.cpp:430:3
    #5 0x168179f in source_locationt::set_line(unsigned int) /home/reuben/development/cbmc/src/java_bytecode/../util/source_location.h:99:5
    #6 0x166cdfe in java_bytecode_parsert::rcode_attribute(java_bytecode_parse_treet::methodt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1125:9
    #7 0x1669ae6 in java_bytecode_parsert::rmethod_attribute(java_bytecode_parse_treet::methodt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1017:7
    #8 0x167747c in java_bytecode_parsert::rmethod(java_bytecode_parse_treet::classt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1567:5
    #9 0x1655577 in java_bytecode_parsert::rmethods(java_bytecode_parse_treet::classt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1515:5
    #10 0x1646ca5 in java_bytecode_parsert::rClassFile() /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:314:3
    #11 0x1644041 in java_bytecode_parsert::parse() /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:219:5
    #12 0x1677b0a in java_bytecode_parse(std::istream&, java_bytecode_parse_treet&, message_handlert&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1591:22
    #13 0x1678e1b in java_bytecode_parse(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, java_bytecode_parse_treet&, message_handlert&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1625:10
    #14 0x129a324 in java_class_loadert::get_parse_tree(java_class_loader_limitt&, dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/java_class_loader.cpp:184:13
    #15 0x1294405 in java_class_loadert::operator()(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/java_class_loader.cpp:62:7
    #16 0x11f05ef in java_bytecode_languaget::parse(std::istream&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:205:5
    #17 0x2d8fad7 in language_uit::parse(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/langapi/language_ui.cpp:128:6
    #18 0x2d8d155 in language_uit::parse() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:74:8
    #19 0x10cfe84 in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:705:10
    #20 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #21 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #22 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #23 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x5dd4d1 in constant_exprt::set_value(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/std_expr.h:3372:5
    #6 0xd2170e in constant_exprt::constant_exprt(dstringt const&, typet const&) /home/reuben/development/cbmc/src/util/./std_expr.h:3362:5
    #7 0x29309ae in set_class_identifier(struct_exprt&, namespacet const&, symbol_typet const&) /home/reuben/development/cbmc/src/goto-programs/builtin_functions.cpp:672:16
    #8 0x2931019 in set_class_identifier(struct_exprt&, namespacet const&, symbol_typet const&) /home/reuben/development/cbmc/src/goto-programs/builtin_functions.cpp:677:5
    #9 0x2934762 in goto_convertt::do_java_new(exprt const&, side_effect_exprt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/builtin_functions.cpp:741:3
    #10 0x247659e in goto_convertt::convert_assign(code_assignt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:966:5
    #11 0x2458295 in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:599:5
    #12 0x246c557 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #13 0x24577af in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #14 0x2466e08 in goto_convertt::convert_label(code_labelt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:448:5
    #15 0x245904c in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:609:5
    #16 0x246c557 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #17 0x24577af in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #18 0x2456e63 in goto_convertt::goto_convert_rec(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:380:3
    #19 0x252e224 in goto_convert_functionst::convert_function(dstringt const&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:256:3
    #20 0x252a4b5 in goto_convert_functionst::goto_convert() /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:91:5
    #21 0x2533afd in goto_convert(symbol_tablet&, goto_functionst&, message_handlert&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:338:5
    #22 0x10d20bf in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:744:5
    #23 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #24 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #25 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #26 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x1289d01 in struct_union_typet::componentt::set_pretty_name(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:215:14
    #6 0x1779014 in java_root_class(symbolt&) /home/reuben/development/cbmc/src/java_bytecode/java_root_class.cpp:36:5
    #7 0x14ab6f4 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:179:5
    #8 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #9 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #10 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #11 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #12 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #13 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #14 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #15 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #16 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #17 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0x5ad637 in exprt::type() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:59:47
    #6 0xb42690 in exprt::make_not() /home/reuben/development/cbmc/src/util/expr.cpp:212:28
    #7 0x2bfc0d6 in goto_symext::symex_goto(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:190:7
    #8 0x2c35219 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:299:5
    #9 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #10 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #11 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #12 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #13 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #14 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #15 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #16 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #17 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #18 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x2a5087e in ssa_exprt::update_identifier() /home/reuben/development/cbmc/src/goto-symex/../util/ssa_expr.h:129:5
    #6 0x2a4e8b7 in ssa_exprt::ssa_exprt(exprt const&) /home/reuben/development/cbmc/src/goto-symex/../util/ssa_expr.h:32:5
    #7 0x2c972ee in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:614:10
    #8 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #9 0x2bfc303 in goto_symext::symex_goto(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:191:7
    #10 0x2c35219 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:299:5
    #11 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #12 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #13 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #14 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #15 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #16 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #17 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #18 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #19 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #20 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5dd5aa in typet::typet(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/type.h:24:39
    #6 0x5dd1d0 in bool_typet::bool_typet() /home/reuben/development/cbmc/src/pointer-analysis/../util/std_types.h:35:16
    #7 0x2bfb06b in goto_symext::symex_goto(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:172:40
    #8 0x2c35219 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:299:5
    #9 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #10 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #11 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #12 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #13 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #14 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #15 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #16 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #17 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #18 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0x5ad637 in exprt::type() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:59:47
    #6 0xd635cb in simplify_exprt::simplify_plus(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr_int.cpp:463:22
    #7 0xcccb6f in simplify_exprt::simplify_node(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2526:12
    #8 0xcd1fc4 in simplify_exprt::simplify_rec(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2634:7
    #9 0xd1e5d8 in simplify_exprt::simplify_node_preorder(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2441:13
    #10 0xcd1e5e in simplify_exprt::simplify_rec(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2632:10
    #11 0xd1e865 in simplify_exprt::simplify(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2684:12
    #12 0xd1ec15 in simplify(exprt&, namespacet const&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2706:10
    #13 0x2a66c4c in goto_symext::do_simplify(exprt&) /home/reuben/development/cbmc/src/goto-symex/goto_symex.cpp:31:5
    #14 0x2b34517 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:283:3
    #15 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #16 0x2b3984b in goto_symext::symex_assign_struct_member(goto_symex_statet&, member_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:499:3
    #17 0x2b2ee76 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:190:7
    #18 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #19 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #20 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #21 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #22 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #23 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #24 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #25 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #26 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #27 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #28 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #29 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0xb4d236 in exprt::sum(exprt const&) /home/reuben/development/cbmc/src/util/expr.cpp:571:5
    #6 0xd638e6 in simplify_exprt::simplify_plus(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr_int.cpp:472:17
    #7 0xcccb6f in simplify_exprt::simplify_node(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2526:12
    #8 0xcd1fc4 in simplify_exprt::simplify_rec(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2634:7
    #9 0xd1e5d8 in simplify_exprt::simplify_node_preorder(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2441:13
    #10 0xcd1e5e in simplify_exprt::simplify_rec(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2632:10
    #11 0xd1e865 in simplify_exprt::simplify(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2684:12
    #12 0xd1ec15 in simplify(exprt&, namespacet const&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2706:10
    #13 0x2a66c4c in goto_symext::do_simplify(exprt&) /home/reuben/development/cbmc/src/goto-symex/goto_symex.cpp:31:5
    #14 0x2b34517 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:283:3
    #15 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #16 0x2b3984b in goto_symext::symex_assign_struct_member(goto_symex_statet&, member_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:499:3
    #17 0x2b2ee76 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:190:7
    #18 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #19 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #20 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #21 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #22 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #23 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #24 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #25 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #26 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #27 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #28 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #29 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c9320 in irept::get_sub() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:241:28
    #4 0x5aef57 in exprt::operands() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:71:25
    #5 0xd1fd84 in to_if_expr(exprt&) /home/reuben/development/cbmc/src/util/./std_expr.h:2569:25
    #6 0xd1e06f in simplify_exprt::simplify_node_preorder(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2435:33
    #7 0xcd1e5e in simplify_exprt::simplify_rec(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2632:10
    #8 0xd1e865 in simplify_exprt::simplify(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2684:12
    #9 0xd1ec15 in simplify(exprt&, namespacet const&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2706:10
    #10 0x2a66c4c in goto_symext::do_simplify(exprt&) /home/reuben/development/cbmc/src/goto-symex/goto_symex.cpp:31:5
    #11 0x2c02cfa in goto_symext::phi_function(goto_symex_statet::goto_statet const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:426:7
    #12 0x2bfef11 in goto_symext::merge_goto(goto_symex_statet::goto_statet const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:295:3
    #13 0x118ca93 in symex_bmct::merge_goto(goto_symex_statet::goto_statet const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:118:3
    #14 0x2bfe97c in goto_symext::merge_gotos(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:268:5
    #15 0x2c33788 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:266:3
    #16 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #17 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #18 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #19 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #20 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #21 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #22 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #23 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #24 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #25 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5b0c67 in exprt::exprt(dstringt const&, typet const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:53:50
    #6 0x14cdbfa in class_typet::baset::baset(typet const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:371:39
    #7 0x14c62f8 in class_typet::add_base(typet const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:390:23
    #8 0x14a8a59 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:134:5
    #9 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #10 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #11 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #12 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #13 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #14 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #15 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #16 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #17 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #18 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5b0c67 in exprt::exprt(dstringt const&, typet const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:53:50
    #6 0x14cdbfa in class_typet::baset::baset(typet const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:371:39
    #7 0x14c62f8 in class_typet::add_base(typet const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:390:23
    #8 0x14a7440 in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:121:5
    #9 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #10 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #11 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #12 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #13 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #14 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #15 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #16 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #17 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #18 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5dd5aa in typet::typet(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/type.h:24:39
    #6 0x128847b in symbol_typet::symbol_typet(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:115:53
    #7 0x14a72dd in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:120:18
    #8 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #9 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #10 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #11 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #12 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #13 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #14 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #15 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #16 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #17 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x1289d01 in struct_union_typet::componentt::set_pretty_name(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:215:14
    #6 0x14a7e2f in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:126:5
    #7 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #8 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #9 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)/home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #10 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #11 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #12 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #13 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #14 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #15 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #16 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x167e551 in source_locationt::set_java_bytecode_index(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/../util/source_location.h:134:5
    #6 0x165e2e8 in java_bytecode_parsert::rbytecode(std::vector<java_bytecode_parse_treet::instructiont, std::allocator<java_bytecode_parse_treet::instructiont> >&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:765:5
    #7 0x1668ae0 in java_bytecode_parsert::rmethod_attribute(java_bytecode_parse_treet::methodt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:995:5
    #8 0x167747c in java_bytecode_parsert::rmethod(java_bytecode_parse_treet::classt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1567:5
    #9 0x1655577 in java_bytecode_parsert::rmethods(java_bytecode_parse_treet::classt&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1515:5
    #10 0x1646ca5 in java_bytecode_parsert::rClassFile() /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:314:3
    #11 0x1644041 in java_bytecode_parsert::parse() /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:219:5
    #12 0x1677b0a in java_bytecode_parse(std::istream&, java_bytecode_parse_treet&, message_handlert&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1591:22
    #13 0x1678e1b in java_bytecode_parse(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, java_bytecode_parse_treet&, message_handlert&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_parser.cpp:1625:10
    #14 0x129a324 in java_class_loadert::get_parse_tree(java_class_loader_limitt&, dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/java_class_loader.cpp:184:13
    #15 0x1294405 in java_class_loadert::operator()(dstringt const&) /home/reuben/development/cbmc/src/java_bytecode/java_class_loader.cpp:62:7
    #16 0x11f05ef in java_bytecode_languaget::parse(std::istream&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:205:5
    #17 0x2d8fad7 in language_uit::parse(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/langapi/language_ui.cpp:128:6
    #18 0x2d8d155 in language_uit::parse() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:74:8
    #19 0x10cfe84 in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:705:10
    #20 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #21 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #22 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #23 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x5dd4d1 in constant_exprt::set_value(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/std_expr.h:3372:5
    #6 0xab7831 in from_integer(BigInt const&, typet const&) /home/reuben/development/cbmc/src/util/arith_tools.cpp:210:5
    #7 0x2406976 in zero_initializert::zero_initializer_rec(typet const&, source_locationt const&) /home/reuben/development/cbmc/src/linking/zero_initializer.cpp:88:18
    #8 0x240f6a6 in zero_initializert::zero_initializer_rec(typet const&, source_locationt const&) /home/reuben/development/cbmc/src/linking/zero_initializer.cpp:224:11
    #9 0x2411da2 in zero_initializert::zero_initializer_rec(typet const&, source_locationt const&) /home/reuben/development/cbmc/src/linking/zero_initializer.cpp:281:18
    #10 0x240f6a6 in zero_initializert::zero_initializer_rec(typet const&, source_locationt const&) /home/reuben/development/cbmc/src/linking/zero_initializer.cpp:224:11
    #11 0x2411da2 in zero_initializert::zero_initializer_rec(typet const&, source_locationt const&) /home/reuben/development/cbmc/src/linking/zero_initializer.cpp:281:18
    #12 0x2416935 in zero_initializert::operator()(typet const&, source_locationt const&) /home/reuben/development/cbmc/src/linking/zero_initializer.cpp:38:12
    #13 0x2414999 in zero_initializer(typet const&, source_locationt const&, namespacet const&, message_handlert&) /home/reuben/development/cbmc/src/linking/zero_initializer.cpp:341:10
    #14 0x2934498 in goto_convertt::do_java_new(exprt const&, side_effect_exprt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/builtin_functions.cpp:740:5
    #15 0x247659e in goto_convertt::convert_assign(code_assignt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:966:5
    #16 0x2458295 in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:599:5
    #17 0x246c557 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #18 0x24577af in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #19 0x2466e08 in goto_convertt::convert_label(code_labelt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:448:5
    #20 0x245904c in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:609:5
    #21 0x246c557 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #22 0x24577af in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #23 0x2456e63 in goto_convertt::goto_convert_rec(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:380:3
    #24 0x252e224 in goto_convert_functionst::convert_function(dstringt const&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:256:3
    #25 0x252a4b5 in goto_convert_functionst::goto_convert() /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:91:5
    #26 0x2533afd in goto_convert(symbol_tablet&, goto_functionst&, message_handlert&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:338:5
    #27 0x10d20bf in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:744:5
    #28 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #29 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5b0c67 in exprt::exprt(dstringt const&, typet const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:53:50
    #6 0x159b95a in symbol_exprt::symbol_exprt(typet const&) /home/reuben/development/cbmc/src/java_bytecode/../util/std_expr.h:94:44
    #7 0x2a4e606 in ssa_exprt::ssa_exprt(exprt const&) /home/reuben/development/cbmc/src/goto-symex/../util/ssa_expr.h:28:5
    #8 0x2c972ee in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:614:10
    #9 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #10 0x2bfc303 in goto_symext::symex_goto(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:191:7
    #11 0x2c35219 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:299:5
    #12 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #13 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #14 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #15 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #16 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #17 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #18 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #19 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #20 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #21 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0xacc3e7 in struct_union_typet::components() /home/reuben/development/cbmc/src/util/./std_types.h:248:28
    #6 0x2c9abfe in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:992:49
    #7 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #8 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #9 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #10 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #11 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #12 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #13 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #14 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #15 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #16 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #17 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #18 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #19 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #20 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #21 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #22 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5dd5aa in typet::typet(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/type.h:24:39
    #6 0x5e011a in type_with_subtypet::type_with_subtypet(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/type.h:120:52
    #7 0xc8dc07 in bitvector_typet::bitvector_typet(dstringt const&, unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1033:5
    #8 0xc8d568 in signedbv_typet::signedbv_typet(unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1187:5
    #9 0x14676de in java_int_type() /home/reuben/development/cbmc/src/java_bytecode/java_types.cpp:33:10
    #10 0x146aa97 in java_type_from_char(char) /home/reuben/development/cbmc/src/java_bytecode/java_types.cpp:283:20
    #11 0x152225b in java_bytecode_convert_methodt::convert_instructions(java_bytecode_parse_treet::methodt const&, code_typet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_method.cpp:1786:26
    #12 0x14f2018 in java_bytecode_convert_methodt::convert(symbolt const&, java_bytecode_parse_treet::methodt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_method.cpp:467:25
    #13 0x15a6205 in java_bytecode_convert_methodt::operator()(symbolt const&, java_bytecode_parse_treet::methodt const&) /home/reuben/development/cbmc/src/java_bytecode/./java_bytecode_convert_method_class.h:52:5
    #14 0x15827e3 in java_bytecode_convert_method(symbolt const&, java_bytecode_parse_treet::methodt const&, symbol_tablet&, message_handlert&, unsigned long,safe_pointer<std::vector<dstringt, std::allocator<dstringt> > >, safe_pointer<std::set<dstringt, std::less<dstringt>, std::allocator<dstringt> > >) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_method.cpp:2777:3
    #15 0x11f8290 in java_bytecode_languaget::do_ci_lazy_method_conversion(symbol_tablet&, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:659:9
    #16 0x11f2631 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:542:8
    #17 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #18 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #19 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #20 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #21 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #22 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #23 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c9320 in irept::get_sub() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:241:28
    #4 0xacc43c in struct_union_typet::components() /home/reuben/development/cbmc/src/util/./std_types.h:248:28
    #5 0x2c9abfe in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:992:49
    #6 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #7 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #8 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #9 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #10 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #11 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #12 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #13 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #14 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #15 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #16 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #17 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #18 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #19 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #20 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #21 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c9320 in irept::get_sub() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:241:28
    #4 0x5aef57 in exprt::operands() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:71:25
    #5 0xcd9eb3 in simplify_exprt::simplify_if(if_exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:1332:35
    #6 0xcc8759 in simplify_exprt::simplify_node(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2483:12
    #7 0xcd1fc4 in simplify_exprt::simplify_rec(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2634:7
    #8 0xd1e865 in simplify_exprt::simplify(exprt&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2684:12
    #9 0xd1ec15 in simplify(exprt&, namespacet const&) /home/reuben/development/cbmc/src/util/simplify_expr.cpp:2706:10
    #10 0x2a66c4c in goto_symext::do_simplify(exprt&) /home/reuben/development/cbmc/src/goto-symex/goto_symex.cpp:31:5
    #11 0x2c02cfa in goto_symext::phi_function(goto_symex_statet::goto_statet const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:426:7
    #12 0x2bfef11 in goto_symext::merge_goto(goto_symex_statet::goto_statet const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:295:3
    #13 0x118ca93 in symex_bmct::merge_goto(goto_symex_statet::goto_statet const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:118:3
    #14 0x2bfe97c in goto_symext::merge_gotos(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:268:5
    #15 0x2c33788 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:266:3
    #16 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #17 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #18 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #19 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #20 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #21 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #22 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #23 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #24 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #25 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0x5ad637 in exprt::type() /home/reuben/development/cbmc/src/pointer-analysis/../util/expr.h:59:47
    #6 0x2c97efc in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:12
    #7 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #8 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #9 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #10 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #11 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #12 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #13 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #14 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #15 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #16 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #17 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #18 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #19 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #20 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #21 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #22 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c9320 in irept::get_sub() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:241:28
    #4 0xacc43c in struct_union_typet::components() /home/reuben/development/cbmc/src/util/./std_types.h:248:28
    #5 0x2c9abfe in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:992:49
    #6 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #7 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #8 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #9 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #10 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #11 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #12 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #13 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #14 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #15 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #16 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #17 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #18 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #19 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #20 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #21 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #22 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0xacc3e7 in struct_union_typet::components() /home/reuben/development/cbmc/src/util/./std_types.h:248:28
    #6 0x2c9abfe in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:992:49
    #7 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #8 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #9 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #10 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #11 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #12 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #13 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #14 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #15 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #16 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #17 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #18 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #19 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #20 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #21 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #22 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #23 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0xc0bb60 in irept::get_named_sub() /home/reuben/development/cbmc/src/util/./irep.h:243:40
    #4 0xbf952a in irept::add(dstringt const&) /home/reuben/development/cbmc/src/util/irep.cpp:508:37
    #5 0xacc3e7 in struct_union_typet::components() /home/reuben/development/cbmc/src/util/./std_types.h:248:28
    #6 0x2c9abfe in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:992:49
    #7 0x2c9b968 in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:1002:9
    #8 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #9 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #10 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #11 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #12 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #13 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #14 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #15 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #16 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #17 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #18 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #19 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #20 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #21 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #22 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #23 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf64d3 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:113:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c9320 in irept::get_sub() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:241:28
    #4 0xacc43c in struct_union_typet::components() /home/reuben/development/cbmc/src/util/./std_types.h:248:28
    #5 0x2c9abfe in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:992:49
    #6 0x2c9b968 in goto_symex_statet::rename(typet&, dstringt const&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:1002:9
    #7 0x2c980b6 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:627:5
    #8 0x2b34347 in goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:282:3
    #9 0x2b2dee5 in goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:181:5
    #10 0x2b2d33b in goto_symext::symex_assign(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:113:5
    #11 0x2b2a65c in goto_symext::symex_assign_rec(goto_symex_statet&, code_assignt const&) /home/reuben/development/cbmc/src/goto-symex/symex_assign.cpp:40:3
    #12 0x2c36dd2 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:337:7
    #13 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #14 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #15 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #16 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #17 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #18 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #19 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #20 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #21 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #22 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5c5119 in irept::irept(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:107:5
    #5 0x5dd5aa in typet::typet(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/type.h:24:39
    #6 0x1460c30 in string_typet::string_typet() /home/reuben/development/cbmc/src/java_bytecode/../util/std_types.h:1476:18
    #7 0x2930902 in set_class_identifier(struct_exprt&, namespacet const&, symbol_typet const&) /home/reuben/development/cbmc/src/goto-programs/builtin_functions.cpp:672:60
    #8 0x2931019 in set_class_identifier(struct_exprt&, namespacet const&, symbol_typet const&) /home/reuben/development/cbmc/src/goto-programs/builtin_functions.cpp:677:5
    #9 0x2934762 in goto_convertt::do_java_new(exprt const&, side_effect_exprt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/builtin_functions.cpp:741:3
    #10 0x247659e in goto_convertt::convert_assign(code_assignt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:966:5
    #11 0x2458295 in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:599:5
    #12 0x246c557 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #13 0x24577af in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #14 0x2466e08 in goto_convertt::convert_label(code_labelt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:448:5
    #15 0x245904c in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:609:5
    #16 0x246c557 in goto_convertt::convert_block(code_blockt const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:742:5
    #17 0x24577af in goto_convertt::convert(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:591:5
    #18 0x2456e63 in goto_convertt::goto_convert_rec(codet const&, goto_programt&) /home/reuben/development/cbmc/src/goto-programs/goto_convert.cpp:380:3
    #19 0x252e224 in goto_convert_functionst::convert_function(dstringt const&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:256:3
    #20 0x252a4b5 in goto_convert_functionst::goto_convert() /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:91:5
    #21 0x2533afd in goto_convert(symbol_tablet&, goto_functionst&, message_handlert&) /home/reuben/development/cbmc/src/goto-programs/goto_convert_functions.cpp:338:5
    #22 0x10d20bf in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:744:5
    #23 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #24 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #25 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #26 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0xbfa9ca in irept::set(dstringt const&, long long) /home/reuben/development/cbmc/src/util/irep.cpp:430:3
    #5 0x2b0956f in ssa_exprt::set_level_2(unsigned int) /home/reuben/development/cbmc/src/goto-symex/../util/ssa_expr.h:96:5
    #6 0x2c9e1b9 in goto_symex_statet::set_ssa_indices(ssa_exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:534:5
    #7 0x2c96a0e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:596:11
    #8 0x2c97569 in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:615:5
    #9 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #10 0x2bfc303 in goto_symext::symex_goto(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:191:7
    #11 0x2c35219 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:299:5
    #12 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #13 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #14 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #15 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #16 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #17 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #18 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #19 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #20 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #21 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0xbfa9ca in irept::set(dstringt const&, long long) /home/reuben/development/cbmc/src/util/irep.cpp:430:3
    #5 0xb9594f in bitvector_typet::set_width(unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1045:5
    #6 0xc8dc5a in bitvector_typet::bitvector_typet(dstringt const&, unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1035:5
    #7 0xc8d568 in signedbv_typet::signedbv_typet(unsigned long) /home/reuben/development/cbmc/src/util/./std_types.h:1187:5
    #8 0x14676de in java_int_type() /home/reuben/development/cbmc/src/java_bytecode/java_types.cpp:33:10
    #9 0x146f852 in java_type_from_string(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_types.cpp:425:20
    #10 0x14abef9 in java_bytecode_convert_classt::convert(symbolt&, java_bytecode_parse_treet::fieldt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:244:20
    #11 0x14aa08c in java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:158:5
    #12 0x14cbcab in java_bytecode_convert_classt::operator()(java_bytecode_parse_treet const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:49:7
    #13 0x14bfc14 in java_bytecode_convert_class(java_bytecode_parse_treet const&, symbol_tablet&, message_handlert&, unsigned long, std::map<dstringt, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*>, std::less<dstringt>, std::allocator<std::pair<dstringt const, std::pair<symbolt const*, java_bytecode_parse_treet::methodt const*> > > >&, lazy_methods_modet, bool) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_convert_class.cpp:499:5
    #14 0x11f20e0 in java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) /home/reuben/development/cbmc/src/java_bytecode/java_bytecode_language.cpp:526:8
    #15 0x381fa4c in language_filest::typecheck(symbol_tablet&) /home/reuben/development/cbmc/src/util/language_file.cpp:223:10
    #16 0x2d90b6e in language_uit::typecheck() /home/reuben/development/cbmc/src/langapi/language_ui.cpp:159:6
    #17 0x10d007f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:707:10
    #18 0x10c3cf0 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:543:5
    #19 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #20 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #21 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0xbfa9ca in irept::set(dstringt const&, long long) /home/reuben/development/cbmc/src/util/irep.cpp:430:3
    #5 0x2a4e6e2 in ssa_exprt::ssa_exprt(exprt const&) /home/reuben/development/cbmc/src/goto-symex/../util/ssa_expr.h:30:5
    #6 0x2c972ee in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:614:10
    #7 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #8 0x2bfc303 in goto_symext::symex_goto(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:191:7
    #9 0x2c35219 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:299:5
    #10 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #11 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #12 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #13 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #14 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #15 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #16 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #17 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #18 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #19 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291

Indirect leak of 128 byte(s) in 1 object(s) allocated from:
    #0 0x558ae0 in operator new(unsigned long) (/home/reuben/development/cbmc/src/cbmc/cbmc+0x558ae0)
    #1 0xbf6126 in irept::detach() /home/reuben/development/cbmc/src/util/irep.cpp:104:10
    #2 0x5c8810 in irept::write() /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:335:5
    #3 0x5c4dd4 in irept::id(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:192:5
    #4 0x5dd73b in irept::set(dstringt const&, dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/irep.h:211:5
    #5 0x5dfcd1 in symbol_exprt::set_identifier(dstringt const&) /home/reuben/development/cbmc/src/pointer-analysis/../util/std_expr.h:111:5
    #6 0x2a50740 in ssa_exprt::update_identifier() /home/reuben/development/cbmc/src/goto-symex/../util/ssa_expr.h:128:5
    #7 0x2a4e8b7 in ssa_exprt::ssa_exprt(exprt const&) /home/reuben/development/cbmc/src/goto-symex/../util/ssa_expr.h:32:5
    #8 0x2c972ee in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:614:10
    #9 0x2c9859e in goto_symex_statet::rename(exprt&, namespacet const&, goto_symex_statet::levelt) /home/reuben/development/cbmc/src/goto-symex/goto_symex_state.cpp:631:7
    #10 0x2bfc303 in goto_symext::symex_goto(goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_goto.cpp:191:7
    #11 0x2c35219 in goto_symext::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:299:5
    #12 0x118b8cf in symex_bmct::symex_step(goto_functionst const&, goto_symex_statet&) /home/reuben/development/cbmc/src/cbmc/symex_bmc.cpp:84:3
    #13 0x2c31b57 in goto_symext::operator()(goto_symex_statet&, goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:177:5
    #14 0x2c3249a in goto_symext::operator()(goto_functionst const&, goto_programt const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:210:3
    #15 0x2c32ee7 in goto_symext::operator()(goto_functionst const&) /home/reuben/development/cbmc/src/goto-symex/symex_main.cpp:235:3
    #16 0xfe0b97 in bmct::run(goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/bmc.cpp:451:5
    #17 0x10dcf24 in cbmc_parse_optionst::do_bmc(bmct&, goto_functionst const&) /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:1048:10
    #18 0x10c5252 in cbmc_parse_optionst::doit() /home/reuben/development/cbmc/src/cbmc/cbmc_parse_options.cpp:567:10
    #19 0x388bab0 in parse_options_baset::main() /home/reuben/development/cbmc/src/util/parse_options.cpp:104:10
    #20 0x1097611 in main /home/reuben/development/cbmc/src/cbmc/cbmc_main.cpp:53:11
    #21 0x7fba7f75982f in __libc_start_main /build/glibc-9tT8Do/glibc-2.23/csu/../csu/libc-start.c:291
reuk commented 7 years ago

Slightly more minimal example which still leaks:

package regression.java.util.Iterator;

import java.util.Iterator;

class DumbIterator implements Iterator {
  private boolean p = true;

  public boolean hasNext() {
    return p;
  }

  public Object next() {
    p = !p;
    return null;
  }
}

public class NoLoop_Pass {
  public static void main(String[] args) {
    ((Iterator)(new DumbIterator())).next();
  }
}
reuk commented 7 years ago

Updated the minimal test case.