diff --git a/regression/cbmc-java/function1/Main.class b/regression/cbmc-java/function1/Main.class
new file mode 100644
index 00000000000..4cb1cb6f542
Binary files /dev/null and b/regression/cbmc-java/function1/Main.class differ
diff --git a/regression/cbmc-java/function1/Main.java b/regression/cbmc-java/function1/Main.java
new file mode 100644
index 00000000000..7152318684e
--- /dev/null
+++ b/regression/cbmc-java/function1/Main.java
@@ -0,0 +1,19 @@
+
+class Other
+{
+  public void fail()
+  {
+    assert i == 0;
+  }
+
+  private int i;
+}
+
+public class Main
+{
+  public static void main(String[] args)
+  {
+    Other o = new Other();
+  }
+}
+
diff --git a/regression/cbmc-java/function1/Other.class b/regression/cbmc-java/function1/Other.class
new file mode 100644
index 00000000000..2ee3eeda9d7
Binary files /dev/null and b/regression/cbmc-java/function1/Other.class differ
diff --git a/regression/cbmc-java/function1/test.desc b/regression/cbmc-java/function1/test.desc
new file mode 100644
index 00000000000..1b33b740986
--- /dev/null
+++ b/regression/cbmc-java/function1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function "java::Other.fail:()V"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/function2/A.class b/regression/cbmc-java/function2/A.class
new file mode 100644
index 00000000000..7af0cd759fb
Binary files /dev/null and b/regression/cbmc-java/function2/A.class differ
diff --git a/regression/cbmc-java/function2/B.class b/regression/cbmc-java/function2/B.class
new file mode 100644
index 00000000000..a47436b1232
Binary files /dev/null and b/regression/cbmc-java/function2/B.class differ
diff --git a/regression/cbmc-java/function2/C.class b/regression/cbmc-java/function2/C.class
new file mode 100644
index 00000000000..8531053409a
Binary files /dev/null and b/regression/cbmc-java/function2/C.class differ
diff --git a/regression/cbmc-java/function2/D.class b/regression/cbmc-java/function2/D.class
new file mode 100644
index 00000000000..02d4e15c990
Binary files /dev/null and b/regression/cbmc-java/function2/D.class differ
diff --git a/regression/cbmc-java/function2/Main.class b/regression/cbmc-java/function2/Main.class
new file mode 100644
index 00000000000..7d091ce7584
Binary files /dev/null and b/regression/cbmc-java/function2/Main.class differ
diff --git a/regression/cbmc-java/function2/Main.java b/regression/cbmc-java/function2/Main.java
new file mode 100644
index 00000000000..7ca39a8e703
--- /dev/null
+++ b/regression/cbmc-java/function2/Main.java
@@ -0,0 +1,34 @@
+
+class A
+{
+  public int i;
+}
+
+class B extends A
+{
+  public int j;
+}
+
+class C extends B
+{
+  public int k;
+}
+
+class D
+{
+  protected C c;
+
+  public void fail()
+  {
+    assert c.i == 0 || c.j == 0 || c.k == 0;
+  }
+}
+
+public class Main
+{
+  public static void main(String[] args)
+  {
+    D d = new D();
+  }
+}
+
diff --git a/regression/cbmc-java/function2/test.desc b/regression/cbmc-java/function2/test.desc
new file mode 100644
index 00000000000..6ce063c8359
--- /dev/null
+++ b/regression/cbmc-java/function2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function "java::D.fail:()V"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/function3/A.class b/regression/cbmc-java/function3/A.class
new file mode 100644
index 00000000000..ed5eaf69452
Binary files /dev/null and b/regression/cbmc-java/function3/A.class differ
diff --git a/regression/cbmc-java/function3/B.class b/regression/cbmc-java/function3/B.class
new file mode 100644
index 00000000000..61ef44f93b6
Binary files /dev/null and b/regression/cbmc-java/function3/B.class differ
diff --git a/regression/cbmc-java/function3/Main.class b/regression/cbmc-java/function3/Main.class
new file mode 100644
index 00000000000..c6720541977
Binary files /dev/null and b/regression/cbmc-java/function3/Main.class differ
diff --git a/regression/cbmc-java/function3/Main.java b/regression/cbmc-java/function3/Main.java
new file mode 100644
index 00000000000..e8aac10625c
--- /dev/null
+++ b/regression/cbmc-java/function3/Main.java
@@ -0,0 +1,22 @@
+
+class A
+{
+  public void dummy() {}
+
+  public B b;
+}
+
+class B
+{
+  public A a;
+}
+
+
+public class Main
+{
+  public static void main(String[] args)
+  {
+    B B = new B();
+  }
+}
+
diff --git a/regression/cbmc-java/function3/test.desc b/regression/cbmc-java/function3/test.desc
new file mode 100644
index 00000000000..fb68b442fdc
--- /dev/null
+++ b/regression/cbmc-java/function3/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function "java::A.dummy:()V"
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 21676f3dd6f..a37cb0c3d0b 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <algorithm>
 #include <set>
+#include <iostream>
 
 #include <util/prefix.h>
 #include <util/std_types.h>
@@ -16,6 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/cprover_prefix.h>
 #include <util/message.h>
+#include <util/config.h>
+#include <util/namespace.h>
+#include <util/pointer_offset_size.h>
+#include <util/i2string.h>
 
 #include <goto-programs/goto_functions.h>
 
@@ -96,6 +101,191 @@ exprt gen_argument(const typet &type)
 
 /*******************************************************************\
 
+Function: gen_nondet_init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+namespace {
+void gen_nondet_init(
+  const exprt &expr,
+  code_blockt &init_code,
+  const namespacet &ns,
+  std::set<irep_idt> &recursion_set,
+  bool is_sub,
+  irep_idt class_identifier)
+{
+  const typet &type=ns.follow(expr.type());
+
+  if(type.id()==ID_struct)
+  {
+    typedef struct_typet::componentt componentt;
+    typedef struct_typet::componentst componentst;
+
+    const struct_typet &struct_type=to_struct_type(type);
+    const irep_idt struct_tag=struct_type.get_tag();
+
+    componentst components=struct_type.components();
+
+    if(!is_sub)
+      class_identifier=struct_tag;
+
+    recursion_set.insert(struct_tag);
+    assert(!recursion_set.empty());
+
+    for(componentst::const_iterator it=components.begin();
+        it!=components.end(); it++)
+    {
+      const componentt &component=*it;
+      const typet &component_type=component.type();
+      irep_idt name=component.get_name();
+
+      member_exprt me(expr, name, component_type);
+
+      if(name=="@class_identifier")
+      {
+        constant_exprt ci(class_identifier, string_typet());
+
+        code_assignt code(me, ci);
+        init_code.copy_to_operands(code);
+      }
+      else
+      {
+        irep_idt new_class_identifier;
+        assert(!name.empty());
+
+        is_sub = name[0]=='@';
+
+        gen_nondet_init(
+          me, init_code, ns, recursion_set, is_sub, class_identifier);
+      }
+    }
+
+    recursion_set.erase(struct_tag);
+  }
+  else if(type.id()!=ID_pointer)
+  {
+    assert(type.id()!= ID_struct);
+
+    side_effect_expr_nondett se=side_effect_expr_nondett(type);
+
+    code_assignt code(expr, se);
+    init_code.copy_to_operands(code);
+  }
+  else
+  {
+    assert(type.id()==ID_pointer);
+
+    // dereferenced type
+    const pointer_typet &pointer_type=to_pointer_type(type);
+    const typet &subtype=ns.follow(pointer_type.subtype());
+
+    if(subtype.id()==ID_struct)
+    {
+      const struct_typet &struct_type=to_struct_type(subtype);
+      const irep_idt struct_tag=struct_type.get_tag();
+
+      if(recursion_set.find(struct_tag)!=recursion_set.end())
+      {
+        // make null
+        null_pointer_exprt null_pointer_expr(pointer_type);
+        code_assignt code(expr, null_pointer_expr);
+        init_code.copy_to_operands(code);
+
+        return;
+      }
+    }
+
+    // build size expression
+    exprt object_size=size_of_expr(subtype, ns);
+
+    if(subtype.id()!=ID_empty && !object_size.is_nil())
+    {
+      // malloc expression
+      side_effect_exprt malloc_expr(ID_malloc);
+      malloc_expr.copy_to_operands(object_size);
+      malloc_expr.type()=pointer_type;
+
+      code_assignt code(expr, malloc_expr);
+      init_code.copy_to_operands(code);
+
+      // dereference expression
+      dereference_exprt deref_expr(expr, subtype);
+
+      gen_nondet_init(deref_expr, init_code, ns, recursion_set, false, "");
+    }
+    else
+    {
+      // make null
+      null_pointer_exprt null_pointer_expr(pointer_type);
+      code_assignt code(expr, null_pointer_expr);
+      init_code.copy_to_operands(code);
+    }
+  }
+}
+}
+
+/*******************************************************************\
+
+Function: gen_nondet_init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+namespace {
+void gen_nondet_init(
+  const exprt &expr,
+  code_blockt &init_code,
+  const namespacet &ns)
+{
+  std::set<irep_idt> recursion_set;
+  gen_nondet_init(expr, init_code, ns, recursion_set, false, "");
+}
+}
+
+/*******************************************************************\
+
+Function: gen_nondet_init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+namespace {
+symbolt &new_tmp_symbol(symbol_tablet &symbol_table)
+{
+  static int temporary_counter=0;
+
+  auxiliary_symbolt new_symbol;
+  symbolt *symbol_ptr;
+
+  do
+  {
+    new_symbol.name="tmp_struct_init$"+i2string(++temporary_counter);
+    new_symbol.base_name=new_symbol.name;
+    new_symbol.mode=ID_java;
+  } while(symbol_table.move(new_symbol, symbol_ptr));
+
+  return *symbol_ptr;
+}
+}
+
+/*******************************************************************\
+
 Function: java_static_lifetime_init
 
   Inputs:
@@ -176,54 +366,138 @@ bool java_entry_point(
      symbol_table.symbols.end())
     return false; // silently ignore
 
-  // are we given a main class?
-  if(main_class.empty())
-    return false; // silently ignore
-  
-  std::string entry_method=
-    id2string(main_class)+".main";
+#if 0
+  std::cout << "Main: " << config.main << std::endl;
+#endif
 
-  std::string prefix="java::"+entry_method+":";
+  messaget message(message_handler);
 
-  // look it up
-  std::set<irep_idt> matches;
+  code_blockt struct_init_code; // struct init code if needed
+  bool have_struct=false;
+  symbol_exprt struct_ptr;
 
-  for(symbol_tablet::symbolst::const_iterator
-      s_it=symbol_table.symbols.begin();
-      s_it!=symbol_table.symbols.end();
-      s_it++)
-  {
-    if(s_it->second.type.id()==ID_code &&
-       has_prefix(id2string(s_it->first), prefix))
-      matches.insert(s_it->first);
-  }
+  symbolt symbol; // main function symbol
 
-  if(matches.empty())
+  // find main symbol
+  if(config.main!="")
   {
-    // Not found, silently ignore
-    return false;
-  }
+    // look it up
+    symbol_tablet::symbolst::const_iterator s_it
+      =symbol_table.symbols.find(config.main);
 
-  if(matches.size()>=2)
-  {
-    messaget message(message_handler);
-    message.error() << "main method in `" << main_class
-                    << "' is ambiguous" << messaget::eom;
-    return true; // give up with error, no main
-  }
+    if(s_it==symbol_table.symbols.end())
+    {
+      message.error() << "main symbol `" << config.main
+                      << "' not found" << messaget::eom;
+      return true;
+    }
+
+    // function symbol
+    symbol=s_it->second;
+
+    if(symbol.type.id()!=ID_code)
+    {
+      message.error() << "main symbol `" << config.main
+                      << "' not a function" << messaget::eom;
+      return true;
+    }
+
+    // check if it has a body
+    if(symbol.value.is_nil())
+    {
+      message.error() << "main method `" << main_class
+                      << "' has no body" << messaget::eom;
+      return true;
+    }
+
+    // get name of associated struct
+    size_t idx=config.main.rfind(".");
+    assert(idx!=std::string::npos);
+    assert(idx<config.main.size());
+    std::string st=config.main.substr(0, idx);
+#if 0
+    std::cout << "Struct name: " << st << std::endl;
+#endif
+
+    // look it up
+    symbol_tablet::symbolst::const_iterator st_it
+      =symbol_table.symbols.find(st);
+
+    if(st_it!=symbol_table.symbols.end() &&
+       st_it->second.type.id()==ID_struct)
+    {
+      const symbolt &struct_symbol=st_it->second;
+      assert(struct_symbol.type.id()==ID_struct);
+      const struct_typet &struct_type=to_struct_type(struct_symbol.type);
+      const pointer_typet pointer_type(struct_type);
 
-  const symbolt &symbol=
-    symbol_table.symbols.find(*matches.begin())->second;
+      symbolt &aux_symbol=new_tmp_symbol(symbol_table);
+      aux_symbol.type=pointer_type;
+      aux_symbol.is_static_lifetime=true;
 
-  // check if it has a body
-  if(symbol.value.is_nil())
+      struct_ptr=aux_symbol.symbol_expr();
+
+      namespacet ns(symbol_table);
+      gen_nondet_init(struct_ptr, struct_init_code, ns);
+
+      have_struct=true;
+    }
+  }
+  else
   {
-    messaget message(message_handler);
-    message.error() << "main method `" << main_class
-                    << "' has no body" << messaget::eom;
-    return true; // give up with error
+    // no function given, we look for the main class
+    assert(config.main=="");
+
+    // are we given a main class?
+    if(main_class.empty())
+      return false; // silently ignore
+
+    std::string entry_method=
+      id2string(main_class)+".main";
+
+    std::string prefix="java::"+entry_method+":";
+
+    // look it up
+    std::set<irep_idt> matches;
+
+    for(symbol_tablet::symbolst::const_iterator
+        s_it=symbol_table.symbols.begin();
+        s_it!=symbol_table.symbols.end();
+        s_it++)
+    {
+      if(s_it->second.type.id()==ID_code &&
+         has_prefix(id2string(s_it->first), prefix))
+        matches.insert(s_it->first);
+    }
+
+    if(matches.empty())
+    {
+      // Not found, silently ignore
+      return false;
+    }
+
+    if(matches.size()>=2)
+    {
+      message.error() << "main method in `" << main_class
+                      << "' is ambiguous" << messaget::eom;
+      return true; // give up with error, no main
+    }
+
+    // function symbol
+    symbol=symbol_table.symbols.find(*matches.begin())->second;
+  
+    // check if it has a body
+    if(symbol.value.is_nil())
+    {
+      message.error() << "main method `" << main_class
+                      << "' has no body" << messaget::eom;
+      return true; // give up with error
+    }
   }
 
+  assert(!symbol.value.is_nil());
+  assert(symbol.type.id()==ID_code);
+
   create_initialize(symbol_table);
 
   if(java_static_lifetime_init(symbol_table, symbol.location, message_handler))
@@ -238,7 +512,6 @@ bool java_entry_point(
 
     if(init_it==symbol_table.symbols.end())
     {
-      messaget message(message_handler);
       message.error() << "failed to find " INITIALIZE " symbol"
                       << messaget::eom;
       return true; // give up with error
@@ -246,12 +519,25 @@ bool java_entry_point(
 
     code_function_callt call_init;
     call_init.lhs().make_nil();
-    call_init.add_source_location() = symbol.location;
+    call_init.add_source_location()=symbol.location;
     call_init.function()=init_it->second.symbol_expr();
 
     init_code.move_to_operands(call_init);
   }
 
+  // add struct init code
+
+  if(have_struct)
+  {
+    typedef code_blockt::operandst operandst;
+    const operandst &operands=struct_init_code.operands();
+
+    for(operandst::const_iterator it=operands.begin(); it!=operands.end(); it++)
+    {
+      init_code.add((const codet&)*it);
+    }
+  }
+
   // build call to main method
 
   code_function_callt call_main;
@@ -264,7 +550,15 @@ bool java_entry_point(
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
 
-  for(unsigned i=0; i<parameters.size(); i++)
+  unsigned i=0;
+
+  if(have_struct && parameters.size()>=1)
+  {
+    main_arguments[0]=struct_ptr;
+    i++;
+  }
+
+  for(; i<parameters.size(); i++)
     main_arguments[i]=gen_argument(parameters[i].type());
 
   call_main.arguments()=main_arguments;
@@ -284,8 +578,6 @@ bool java_entry_point(
 
   if(symbol_table.move(new_symbol))
   {
-    messaget message;
-    message.set_message_handler(message_handler);
     message.error() << "failed to move main symbol" << messaget::eom;
     return true;
   }