void java_internal_additions(symbol_tablet &dest)
{
  // add __CPROVER_rounding_mode

  {
    symbolt symbol;
    symbol.base_name="__CPROVER_rounding_mode";
    symbol.name=CPROVER_PREFIX "rounding_mode";
    symbol.type=signed_int_type();
    symbol.mode=ID_C;
    symbol.is_lvalue=true;
    symbol.is_state_var=true;
    symbol.is_thread_local=true;
    dest.add(symbol);
  }

  // add __CPROVER_malloc_object

  {
    symbolt symbol;
    symbol.base_name="__CPROVER_malloc_object";
    symbol.name=CPROVER_PREFIX "malloc_object";
    symbol.type=pointer_type(empty_typet());
    symbol.mode=ID_C;
    symbol.is_lvalue=true;
    symbol.is_state_var=true;
    symbol.is_thread_local=true;
    dest.add(symbol);
  }
}

/// Remove the body of function "identifier" such that an analysis will treat it
/// as a side-effect free function with non-deterministic return value.
/// \par parameters: symbol_table  Input symbol table to be modified
/// goto_functions  Input functions to be modified
/// identifier  Function to be removed
/// message_handler  Error/status output
void remove_function(
  symbol_tablet &symbol_table,
  goto_functionst &goto_functions,
  const irep_idt &identifier,
  message_handlert &message_handler)
{
  messaget message(message_handler);

  goto_functionst::function_mapt::iterator entry=
    goto_functions.function_map.find(identifier);

  if(entry==goto_functions.function_map.end())
  {
    message.error() << "No function " << identifier
                    << " in goto program" << messaget::eom;
    return;
  }
  else if(entry->second.is_inlined())
  {
    message.warning() << "Function " << identifier << " is inlined, "
                      << "instantiations will not be removed"
                      << messaget::eom;
  }

  if(entry->second.body_available())
  {
    message.status() << "Removing body of " << identifier
                     << messaget::eom;
    entry->second.clear();
    symbol_table.lookup(identifier).value.make_nil();
  }
}

void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table)
{
  if(!symbol.is_lvalue) return;
  
  if(symbol.type.get(ID_C_failed_symbol)!="")
    return;

  if(symbol.type.id()==ID_pointer)
  {
    symbolt new_symbol;
    new_symbol.is_lvalue=true;
    new_symbol.module=symbol.module;
    new_symbol.mode=symbol.mode;
    new_symbol.base_name=failed_symbol_id(symbol.base_name);
    new_symbol.name=failed_symbol_id(symbol.name);
    new_symbol.type=symbol.type.subtype();
    new_symbol.value.make_nil();
    new_symbol.type.set(ID_C_is_failed_symbol, true);
    
    symbol.type.set(ID_C_failed_symbol, new_symbol.name);
    
    if(new_symbol.type.id()==ID_pointer)
      add_failed_symbol(new_symbol, symbol_table); // recursive call
        
    symbol_table.move(new_symbol);
  }
}

std::string get_prog_var_name(const symbol_tablet &st,
    const goto_programt::targett &decl)
{
  const irep_idt &base_id=st.lookup(get_affected_variable(*decl)).base_name;
  std::string base_name(id2string(base_id));
  return base_name+=PROG_SUFFIX;
}

dereference_exprt cegis_operand(const symbol_tablet &st,
    const std::string &func_name, const typet &type, const size_t op)
{
  const member_exprt operand_id(cegis_operand_id(st, func_name, op));
  const std::string array_name(cegis_operand_array_name(st, type));
  const symbol_exprt array(st.lookup(array_name).symbol_expr());
  return dereference_exprt(index_exprt(array, operand_id), type);
}

goto_programt::targett assign_jsa_meta_variable(const symbol_tablet &st,
    goto_functionst &gf, const goto_programt::targett &pos,
    const std::string &base_name, const exprt &expr_value)
{
  const std::string name(get_cegis_meta_name(base_name));
  const symbol_exprt lhs(st.lookup(name).symbol_expr());
  return jsa_assign(st, gf, pos, lhs, expr_value);
}

code_function_callt function_to_call(
  symbol_tablet &symbol_table,
  const irep_idt &id,
  const irep_idt &argument)
{
  // already there?

  symbol_tablet::symbolst::const_iterator s_it=
    symbol_table.symbols.find(id);

  if(s_it==symbol_table.symbols.end())
  {
    // not there
    pointer_typet p(char_type());
    p.subtype().set(ID_C_constant, true);

    code_typet function_type;
    function_type.return_type()=empty_typet();
    function_type.parameters().push_back(
      code_typet::parametert(p));

    symbolt new_symbol;
    new_symbol.name=id;
    new_symbol.base_name=id;
    new_symbol.type=function_type;

    symbol_table.move(new_symbol);

    s_it=symbol_table.symbols.find(id);
    assert(s_it!=symbol_table.symbols.end());
  }

  // signature is expected to be
  // (type *) -> ...
  if(s_it->second.type.id()!=ID_code ||
     to_code_type(s_it->second.type).parameters().size()!=1 ||
     to_code_type(s_it->second.type).parameters()[0].type().id()!=ID_pointer)
  {
    std::string error="function `"+id2string(id)+"' has wrong signature";
    throw error;
  }

  string_constantt function_id_string(argument);

  code_function_callt call;
  call.lhs().make_nil();
  call.function()=
    symbol_exprt(s_it->second.name, s_it->second.type);
  call.arguments().resize(1);
  call.arguments()[0]=
    typecast_exprt(
      address_of_exprt(
        index_exprt(
          function_id_string, from_integer(0, index_type()))),
      to_code_type(s_it->second.type).parameters()[0].type());

  return call;
}

void execute_inv_prog(const symbol_tablet &st, goto_functionst &gf,
    const size_t max_solution_size, const goto_programt::targett &decl,
    const std::string &prog_base_name)
{
  goto_programt &body=get_entry_body(gf);
  goto_programt::targett pos=decl;
  goto_programt::targett execution=body.insert_after(++pos);
  execution->type=goto_program_instruction_typet::FUNCTION_CALL;
  execution->source_location=default_cegis_source_location();
  code_function_callt call;
  call.function()=st.lookup(DANGER_EXECUTE).symbol_expr();
  const std::string prog_name(get_cegis_meta_name(prog_base_name));
  const symbol_exprt prog_symbol(st.lookup(prog_name).symbol_expr());
  const typet size_type(unsigned_int_type());
  const constant_exprt index(from_integer(0u, size_type));
  const index_exprt first_elem(prog_symbol, index);
  call.arguments().push_back(address_of_exprt(first_elem));
  const constant_exprt size(from_integer(max_solution_size, size_type));
  call.arguments().push_back(size);
  execution->code=call;
}

void propagate_controller_sizes(const symbol_tablet &st, goto_functionst &gf)
{
  const symbolt &symbol=st.lookup(CEGIS_CONTROL_SOLUTION_VAR_NAME);
  const struct_exprt &controller_value=to_struct_expr(symbol.value);
  const namespacet ns(st);
  const exprt &a_size=get_a_size(ns, controller_value);
  const exprt &b_size=get_b_size(ns, controller_value);
  replace_sizes_visitort visitor(a_size, b_size);
  goto_programt &body=get_entry_body(gf);
  for (goto_programt::instructiont &instr : body.instructions)
  {
    instr.code.visit(visitor);
    instr.guard.visit(visitor);
  }
}

bool java_static_lifetime_init(
  symbol_tablet &symbol_table,
  const source_locationt &source_location,
  message_handlert &message_handler)
{
  symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE);
  code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
  
  // we need to zero out all static variables
  
  for(symbol_tablet::symbolst::const_iterator
      it=symbol_table.symbols.begin();
      it!=symbol_table.symbols.end();
      it++)
  {
    if(it->second.type.id()!=ID_code &&
       it->second.is_lvalue &&
       it->second.is_state_var &&
       it->second.is_static_lifetime &&
       it->second.value.is_not_nil() &&
       it->second.mode==ID_java)
    {
      code_assignt assignment(it->second.symbol_expr(), it->second.value);
      code_block.add(assignment);
    }
  }
  
  // we now need to run all the <clinit> methods

  for(symbol_tablet::symbolst::const_iterator
      it=symbol_table.symbols.begin();
      it!=symbol_table.symbols.end();
      it++)
  {
    if(it->second.base_name=="<clinit>" &&
       it->second.type.id()==ID_code &&
       it->second.mode==ID_java)
    {
      code_function_callt function_call;
      function_call.lhs()=nil_exprt();
      function_call.function()=it->second.symbol_expr();
      code_block.add(function_call);
    }
  }
  
  return false;
}

symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
{
  const irep_idt identifier="$stack_depth";
  signedbv_typet type(sizeof(int)*8);

  symbolt new_symbol;
  new_symbol.name=identifier;
  new_symbol.base_name=identifier;
  new_symbol.pretty_name=identifier;
  new_symbol.type=type;
  new_symbol.is_static_lifetime=true;
  new_symbol.value=from_integer(0, type);
  new_symbol.mode=ID_C;
  new_symbol.is_thread_local=true;
  new_symbol.is_lvalue=true;

  symbol_table.move(new_symbol);

  return symbol_exprt(identifier, type);
}

bool java_bytecode_languaget::typecheck(
  symbol_tablet &symbol_table,
  const std::string &module)
{
  symbol_tablet new_symbol_table;

  if(java_bytecode_convert(
       parse_tree, new_symbol_table, module, get_message_handler()))
    return true;
  
  if(java_bytecode_typecheck(
       new_symbol_table, module, get_message_handler()))
    return true;

  symbol_table.swap(new_symbol_table);

//  if(linking(new_symbol_table, symbol_table, message_handler))
//    return true;
    
  return false;
}

bool read_goto_object(
  std::istream &in,
  const std::string &filename,
  symbol_tablet &symbol_table,
  goto_functionst &functions,
  message_handlert &message_handler)
{
  messaget message(message_handler);

  xml_parser.clear();
  xml_parser.filename = filename;
  xml_parser.in = ∈
  xml_parser.set_message_handler(message_handler);

  if (xml_parser.parse())
    return true;

  xmlt &top = xml_parser.parse_tree.element;

  if (top.get_attribute("version")!=XML_VERSION)
  {
    message.error() <<
      "The input was compiled with a different version of "
      "goto-cc, please recompile." << messaget::eom;
    return true;
  }

  xml_irep_convertt::ireps_containert ic;
  xml_irep_convertt irepconverter(ic);
  xml_symbol_convertt symbolconverter(ic);
  xml_goto_function_convertt gfconverter(ic);

  if(top.name.substr(0, 11)=="goto-object")
  {
    for(xmlt::elementst::const_iterator
        sec_it=top.elements.begin();
        sec_it != top.elements.end();
        sec_it++)
    {
      xmlt sec = *sec_it;
      if (sec.name=="irep_hash_map")
      {
        for(xmlt::elementst::const_iterator
            irep_it = sec.elements.begin();
            irep_it != sec.elements.end();
            irep_it++)
        {
          irept i;
          irepconverter.convert(*irep_it, i);
          irepconverter.insert(irep_it->get_attribute("id"), i);
        }
      }
      else if (sec.name=="symbols")
      {
        for(xmlt::elementst::const_iterator
            sym_it = sec.elements.begin();
            sym_it != sec.elements.end();
            sym_it++)
        {
          symbolt symbol;
          symbolconverter.convert(*sym_it, symbol);
          // std::cout << "Adding Symbol: " << symbol.name << std::endl;
          if(!symbol.is_type &&
             symbol.type.id()=="code")
          {
            // makes sure there is an empty function
            // for this symbol. if we got code for it,
            // it will be added lateron.
            functions.function_map[symbol.name].type=
              to_code_type(symbol.type);
          }
          symbol_table.add(symbol);
        }
      }
      else if (sec.name=="functions")
      {
        for(xmlt::elementst::const_iterator
            fun_it = sec.elements.begin();
            fun_it != sec.elements.end();
            fun_it++)
        {
          std::string fname = fun_it->get_attribute("name");
          //std::cout << "Adding function body: " << fname << std::endl;
          goto_functionst::goto_functiont &f = functions.function_map[fname];
          gfconverter.convert(*fun_it, f);
        }
      }
      else
      {
        message.error() << "Unknown Section '" << sec.name
                        << "' in object file." << messaget::eom;
        return true;
      }

    }
  }
  else
  {
    message.error() << "no goto-object" << messaget::eom;
    return true;
//.........这里部分代码省略.........

bool java_entry_point(
  symbol_tablet &symbol_table,
  const irep_idt &main_class,
  message_handlert &message_handler)
{
  // check if the entry point is already there
  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
     symbol_table.symbols.end())
    return false; // silently ignore

  messaget message(message_handler);

  symbolt symbol; // main function symbol

  // find main symbol
  if(config.main!="")
  {
    // Add java:: prefix
    std::string main_identifier="java::"+config.main;
    
    symbol_tablet::symbolst::const_iterator s_it;
    
    // Does it have a type signature? (':' suffix)
    if(config.main.rfind(':')==std::string::npos)
    {
      std::string prefix=main_identifier+':';
      std::set<irep_idt> matches;
      
      for(const auto & s : symbol_table.symbols)
        if(has_prefix(id2string(s.first), prefix) &&
           s.second.type.id()==ID_code)
          matches.insert(s.first);

      if(matches.empty())
      {
        message.error() << "main symbol `" << config.main
                        << "' not found" << messaget::eom;
        return true;
      }
      else if(matches.size()==1)
      {
        s_it=symbol_table.symbols.find(*matches.begin());
        assert(s_it!=symbol_table.symbols.end());
      }
      else
      {
        message.error() << "main symbol `" << config.main
                        << "' is ambiguous:\n";

        for(const auto & s : matches)
          message.error() << "  " << s << '\n';
        
        message.error() << messaget::eom;

        return true;
      }
    }
    else
    {
      // just look it up
      s_it=symbol_table.symbols.find(main_identifier);

      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;
    }
  }
  else
  {
    // 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";

//.........这里部分代码省略.........

size_t get_size(const symbol_tablet &st, const char * const id)
{
  return to_size(to_array_type(st.lookup(id).type).size());
}

bool read_bin_goto_object_v3(
  std::istream &in,
  const std::string &filename,
  symbol_tablet &symbol_table,
  goto_functionst &functions,
  message_handlert &message_handler,
  irep_serializationt &irepconverter)
{
  std::size_t count = irepconverter.read_gb_word(in); // # of symbols

  for(std::size_t i=0; i<count; i++)
  {
    symbolt sym;

    irepconverter.reference_convert(in, sym.type);
    irepconverter.reference_convert(in, sym.value);
    irepconverter.reference_convert(in, sym.location);

    sym.name = irepconverter.read_string_ref(in);
    sym.module = irepconverter.read_string_ref(in);
    sym.base_name = irepconverter.read_string_ref(in);
    sym.mode = irepconverter.read_string_ref(in);
    sym.pretty_name = irepconverter.read_string_ref(in);

    // obsolete: symordering
    irepconverter.read_gb_word(in);

    std::size_t flags=irepconverter.read_gb_word(in);

    sym.is_weak = (flags &(1 << 16))!=0;
    sym.is_type = (flags &(1 << 15))!=0;
    sym.is_property = (flags &(1 << 14))!=0;
    sym.is_macro = (flags &(1 << 13))!=0;
    sym.is_exported = (flags &(1 << 12))!=0;
    sym.is_input = (flags &(1 << 11))!=0;
    sym.is_output = (flags &(1 << 10))!=0;
    sym.is_state_var = (flags &(1 << 9))!=0;
    sym.is_parameter = (flags &(1 << 8))!=0;
    sym.is_auxiliary = (flags &(1 << 7))!=0;
    // sym.binding = (flags &(1 << 6))!=0;
    sym.is_lvalue = (flags &(1 << 5))!=0;
    sym.is_static_lifetime = (flags &(1 << 4))!=0;
    sym.is_thread_local = (flags &(1 << 3))!=0;
    sym.is_file_local = (flags &(1 << 2))!=0;
    sym.is_extern = (flags &(1 << 1))!=0;
    sym.is_volatile = (flags &1)!=0;

    if(!sym.is_type && sym.type.id()==ID_code)
    {
      // makes sure there is an empty function
      // for every function symbol and fixes
      // the function types.
      functions.function_map[sym.name].type=to_code_type(sym.type);
    }

    symbol_table.add(sym);
  }

  count=irepconverter.read_gb_word(in); // # of functions

  for(std::size_t i=0; i<count; i++)
  {
    irep_idt fname=irepconverter.read_gb_string(in);
    goto_functionst::goto_functiont &f = functions.function_map[fname];

    typedef std::map<goto_programt::targett, std::list<unsigned> > target_mapt;
    target_mapt target_map;
    typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
    rev_target_mapt rev_target_map;

    bool hidden=false;

    std::size_t ins_count = irepconverter.read_gb_word(in); // # of instructions
    for(std::size_t i=0; i<ins_count; i++)
    {
      goto_programt::targett itarget = f.body.add_instruction();
      goto_programt::instructiont &instruction=*itarget;

      irepconverter.reference_convert(in, instruction.code);
      instruction.function = irepconverter.read_string_ref(in);
      irepconverter.reference_convert(in, instruction.source_location);
      instruction.type = (goto_program_instruction_typet)
                              irepconverter.read_gb_word(in);
      instruction.guard.make_nil();
      irepconverter.reference_convert(in, instruction.guard);
      irepconverter.read_string_ref(in); // former event
      instruction.target_number = irepconverter.read_gb_word(in);
      if(instruction.is_target() &&
         rev_target_map.insert(
           rev_target_map.end(),
           std::make_pair(instruction.target_number, itarget))->second!=itarget)
        assert(false);

      std::size_t t_count = irepconverter.read_gb_word(in); // # of targets
      for(std::size_t i=0; i<t_count; i++)
        // just save the target numbers
        target_map[itarget].push_back(irepconverter.read_gb_word(in));

      std::size_t l_count = irepconverter.read_gb_word(in); // # of labels

//.........这里部分代码省略.........