void show_properties_json(
  json_arrayt &json_properties,
  const namespacet &ns,
  const irep_idt &identifier,
  const goto_programt &goto_program)
{
  for(const auto &ins : goto_program.instructions)
  {
    if(!ins.is_assert())
      continue;

    const source_locationt &source_location=ins.source_location;

    const irep_idt &comment=source_location.get_comment();
    // const irep_idt &function=location.get_function();
    const irep_idt &property_class=source_location.get_property_class();
    const irep_idt description=
      (comment==""?"assertion":comment);

    irep_idt property_id=source_location.get_property_id();

    json_objectt &json_property=
      json_properties.push_back(jsont()).make_object();
    json_property["name"]=json_stringt(id2string(property_id));
    json_property["class"]=json_stringt(id2string(property_class));
    json_property["sourceLocation"]=json(source_location);
    json_property["description"]=json_stringt(id2string(description));
    json_property["expression"]=
      json_stringt(from_expr(ns, identifier, ins.guard));
  }
}

void fault_localizationt::report(irep_idt goal_id)
{
  if(goal_id==ID_nil)
    goal_id=failed->source.pc->source_location.get_property_id();

  lpointst &lpoints = lpoints_map[goal_id];

  if(lpoints.empty())
  {
    status() << "["+id2string(goal_id)+"]: \n"
                   << "   unable to localize fault"
                   << eom;
    return;
  }

  debug() << "Fault localization scores:" << eom;
  lpointt &max=lpoints.begin()->second;
  for(auto &l : lpoints)
  {
    debug() << l.second.target->source_location
            << "\n  score: " << l.second.score << eom;
    if(max.score<l.second.score)
      max=l.second;
  }
  status() << "["+id2string(goal_id)+"]: \n"
                   << "  " << max.target->source_location
                   << eom;
}

void graphml_witness_extt::add_edge(
  const graphmlt::node_indext &from,
  const dynamic_cfg_nodet &from_cfg_node,
  const graphmlt::node_indext &to,
  const dynamic_cfg_nodet &to_cfg_node)
{
  const source_locationt &source_location=from_cfg_node.id.pc->source_location;

  xmlt edge("edge");
  edge.set_attribute("source", graphml[from].node_name);
  edge.set_attribute("target", graphml[to].node_name);

  {
    xmlt &data_f=edge.new_element("data");
    data_f.set_attribute("key", "originfile");
    data_f.data=id2string(source_location.get_file());

    xmlt &data_l=edge.new_element("data");
    data_l.set_attribute("key", "startline");
    data_l.data=id2string(source_location.get_line());

    if(to_cfg_node.is_loop_head)
    {
      xmlt &data_l=edge.new_element("data");
      data_l.set_attribute("key", "enterLoopHead");
      data_l.data="true";
    }
  }

  graphml[to].in[from].xml_node=edge;
  graphml[from].out[to].xml_node=edge;
}

irep_idt cpp_declarator_convertert::get_pretty_name()
{
    if(is_code)
    {
        const irept::subt &parameters=
            final_type.find(ID_parameters).get_sub();

        std::string result=scope->prefix+id2string(base_name)+"(";

        forall_irep(it, parameters)
        {
            const typet &parameter_type=((exprt &)*it).type();

            if(it!=parameters.begin())
                result+=", ";

            result+=cpp_typecheck.to_string(parameter_type);
        }

        result+=')';

        return result;
    }

    return scope->prefix+id2string(base_name);
}

void component_exprt::gen_loc_var(
    exprt &loc_var,
    const exprt &expr, 
    std::string suffix)
{
  std::string base;
  if (expr.id()==ID_symbol)
    base="."+id2string(to_symbol_expr(expr).get_identifier());
  else if (expr.id()==ID_constant)
    base=".const";
  else if (expr.id()==ID_typecast)
  {
    base=".typecast__"+id2string(expr.type().id());
    if (expr.type().id()==ID_signedbv)
    {
      base=base+i2string(to_signedbv_type(expr.type()).get_width());
    }
    else if (expr.type().id()==ID_unsignedbv)
    {
      base=base+i2string(to_unsignedbv_type(expr.type()).get_width());
    }
  }
  else if(id_maps.find(expr.id())!=id_maps.end())
    base=".OPERATOR."+id_maps[expr.id()];
  else
    base=".OPERATOR."+id2string(expr.id());
  std::string final_name="L."+id2string(source_location.get_line())+"."+i2string(instruction_number)+"_"+i2string(component_cnt)+"_"+i2string(unique_identifier)+base+suffix;
  //typet type(ID_integer);
  //exprt loc_var(ID_symbol, type);
  to_symbol_expr(loc_var).set_identifier(final_name);
}

void java_bytecode_convertt::generate_class_stub(const irep_idt &class_name)
{
  class_typet class_type;

  class_type.set_tag(class_name);
  class_type.set(ID_base_name, class_name);

  class_type.set(ID_incomplete_class, true);

  // produce class symbol
  symbolt new_symbol;
  new_symbol.base_name=class_name;
  new_symbol.pretty_name=class_name;
  new_symbol.name="java::"+id2string(class_name);
  class_type.set(ID_name, new_symbol.name);
  new_symbol.type=class_type;
  new_symbol.mode=ID_java;
  new_symbol.is_type=true;
  
  symbolt *class_symbol;
  
  if(symbol_table.move(new_symbol, class_symbol))
  {
    warning() << "stub class symbol "+id2string(new_symbol.name)+" already exists";
  }
  else
  {
    // create the class identifier
    create_class_identifier(*class_symbol);
  }
}

std::unique_ptr<languaget> get_language(
  const namespacet &ns,
  const irep_idt &identifier)
{
  if(identifier=="")
    return std::unique_ptr<languaget>(get_default_language());
  else
  {
    const symbolt *symbol;
    
    if(ns.lookup(identifier, symbol))
      return std::unique_ptr<languaget>(get_default_language());
    else if(symbol->mode=="")
      return std::unique_ptr<languaget>(get_default_language());
    else
    {
      languaget *ptr=get_language_from_mode(symbol->mode);

      if(ptr==NULL)
        throw "symbol `"+id2string(symbol->name)+
              "' has unknown mode '"+id2string(symbol->mode)+"'";

      return std::unique_ptr<languaget>(ptr);
    }
  }
}

var_mapt::var_infot & var_mapt::operator()(
  const irep_idt &symbol,
  const irep_idt &suffix,
  const typet &type)
{
  assert(symbol!=irep_idt());

  std::string full_identifier=
    id2string(symbol)+id2string(suffix);

  std::pair<id_mapt::iterator, bool> result;

  result=id_map.insert(std::pair<irep_idt, var_infot>(
    full_identifier, var_infot()));

  if(result.second) // inserted?
  {
    result.first->second.full_identifier=full_identifier;
    result.first->second.symbol=symbol;
    result.first->second.suffix=suffix;
    result.first->second.type=type;
    init(result.first->second);
  }

  return result.first->second;
}

bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
{
  if(type1 == type2)
    return true;

  if(type1.id() == "symbol")
  {
    const symbolt &symbol = ns.lookup(type1);
    if(!symbol.is_type)
      throw "symbol " + id2string(symbol.name) + " is not a type";

    return type_eq(symbol.type, type2, ns);
  }

  if(type2.id() == "symbol")
  {
    const symbolt &symbol = ns.lookup(type2);
    if(!symbol.is_type)
      throw "symbol " + id2string(symbol.name) + " is not a type";

    return type_eq(type1, symbol.type, ns);
  }

  return false;
}

void cpp_declarator_convertert::get_final_identifier()
{
  std::string identifier=id2string(base_name);

  // main is always "C" linkage, as a matter of principle
  if(is_code &&
     base_name==ID_main &&
     scope->prefix=="")
  {
    linkage_spec=ID_C;
  }

  if(is_code)
  {
    // is there already an `extern "C"' function with the same name?
    
    if(linkage_spec==ID_auto &&
       scope->prefix=="" &&
       cpp_typecheck.context.symbols.find("c::"+identifier)!=
       cpp_typecheck.context.symbols.end())
    {
    }
    else if(linkage_spec!=ID_C)
    {
      // add C++ decoration
      identifier+=id2string(cpp_typecheck.function_identifier(final_type));
    }
  }

  final_identifier=
    "c::"+
    scope->prefix+
    identifier;
}

void java_class_loadert::read_jar_file(
  java_class_loader_limitt &class_loader_limit,
  const irep_idt &file)
{
  // done already?
  if(jar_map.find(file)!=jar_map.end())
    return;

  jar_filet &jar_file=jar_pool(class_loader_limit, id2string(file));

  if(!jar_file)
  {
    error() << "failed to open JAR file `" << file << "'" << eom;
    return;
  }

  debug() << "adding JAR file `" << file << "'" << eom;

  auto &jm=jar_map[file];

  for(auto &jar_entry : jar_file.filtered_jar)
  {
    std::string file_name=id2string(jar_entry.first);

    // does it end on .class?
    if(has_suffix(file_name, ".class"))
    {
      irep_idt class_name=file_to_class_name(file_name);

      // record
      jm.entries[class_name].class_file_name=file_name;
    }
  }
}

std::string array_name(
  const namespacet &ns,
  const exprt &expr)
{
  if(expr.id()==ID_index)
  {
    if(expr.operands().size()!=2)
      throw "index takes two operands";

    return array_name(ns, expr.op0())+"[]";
  }
  else if(is_ssa_expr(expr))
  {
    const symbolt &symbol=
      ns.lookup(to_ssa_expr(expr).get_object_name());
    return "array `"+id2string(symbol.base_name)+"'";
  }
  else if(expr.id()==ID_symbol)
  {
    const symbolt &symbol=ns.lookup(expr);
    return "array `"+id2string(symbol.base_name)+"'";
  }
  else if(expr.id()==ID_string_constant)
  {
    return "string constant";
  }
  else if(expr.id()==ID_member)
  {
    assert(expr.operands().size()==1);
    return array_name(ns, expr.op0())+"."+
           expr.get_string(ID_component_name);
  }

  return "array";
}

void show_properties(
  const namespacet &ns,
  const irep_idt &identifier,
  ui_message_handlert::uit ui,
  const goto_programt &goto_program)
{
  for(const auto &ins : goto_program.instructions)
  {
    if(!ins.is_assert())
      continue;

    const source_locationt &source_location=ins.source_location;

    const irep_idt &comment=source_location.get_comment();
    const irep_idt &property_class=source_location.get_property_class();
    const irep_idt description=
      (comment==""?"assertion":comment);

    irep_idt property_id=source_location.get_property_id();

    switch(ui)
    {
    case ui_message_handlert::uit::XML_UI:
      {
        // use me instead
        xmlt xml_property("property");
        xml_property.set_attribute("name", id2string(property_id));
        xml_property.set_attribute("class", id2string(property_class));

        xmlt &property_l=xml_property.new_element();
        property_l=xml(source_location);

        xml_property.new_element("description").data=id2string(description);
        xml_property.new_element("expression").data=
          from_expr(ns, identifier, ins.guard);

        std::cout << xml_property << '\n';
      }
      break;

    case ui_message_handlert::uit::JSON_UI:
      UNREACHABLE;
      break;

    case ui_message_handlert::uit::PLAIN:
      std::cout << "Property " << property_id << ":\n";

      std::cout << "  " << ins.source_location << '\n'
                << "  " << description << '\n'
                << "  " << from_expr(ns, identifier, ins.guard)
                        << '\n';

      std::cout << '\n';
      break;

    default:
      UNREACHABLE;
    }
  }
}

void java_bytecode_convert_classt::convert(
  symbolt &class_symbol,
  const fieldt &f)
{
  typet field_type=java_type_from_string(f.signature);

  // is this a static field?
  if(f.is_static)
  {
    // Create the symbol; we won't add to the struct type.
    symbolt new_symbol;

    new_symbol.is_static_lifetime=true;
    new_symbol.is_lvalue=true;
    new_symbol.is_state_var=true;
    new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
    new_symbol.base_name=f.name;
    new_symbol.type=field_type;
    new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
      "."+id2string(f.name);
    new_symbol.mode=ID_java;
    new_symbol.is_type=false;
    const namespacet ns(symbol_table);
    new_symbol.value=
      zero_initializer(
        field_type,
        class_symbol.location,
        ns,
        get_message_handler());

    // Do we have the static field symbol already?
    const auto s_it=symbol_table.symbols.find(new_symbol.name);
    if(s_it!=symbol_table.symbols.end())
      symbol_table.symbols.erase(s_it); // erase, we stubbed it

    if(symbol_table.add(new_symbol))
      assert(false && "failed to add static field symbol");
  }
  else
  {
    class_typet &class_type=to_class_type(class_symbol.type);

    class_type.components().push_back(class_typet::componentt());
    class_typet::componentt &component=class_type.components().back();

    component.set_name(f.name);
    component.set_base_name(f.name);
    component.set_pretty_name(f.name);
    component.type()=field_type;

    if(f.is_private)
      component.set_access(ID_private);
    else if(f.is_protected)
      component.set_access(ID_protected);
    else if(f.is_public)
      component.set_access(ID_public);
  }
}

bool is_jsa_heap(const typet &type)
{
  const irep_idt &type_id=type.id();
  if (ID_symbol == type_id)
    return id2string(to_symbol_type(type).get_identifier()) == JSA_HEAP_TAG;
  if (ID_struct != type_id) return false;
  const irep_idt tag(to_struct_type(type).get_tag());
  return id2string(tag) == JSA_HEAP_TAG;
}

  Forall_goto_program_instructions(i_it, goto_program)
  {
    if(i_it->is_function_call())
    {
      code_function_callt &function_call=to_code_function_call(i_it->code);

      code_typet old_type=to_code_type(function_call.function().type());

      // Do we return anything?
      if(old_type.return_type()!=empty_typet())
      {
        // replace "lhs=f(...)" by "f(...); lhs=f#return_value; DEAD f#return_value;"
        assert(function_call.function().id()==ID_symbol);

        const irep_idt function_id=
          to_symbol_expr(function_call.function()).get_identifier();

        // see if we have a body
        goto_functionst::function_mapt::const_iterator
          f_it=goto_functions.function_map.find(function_id);

        if(f_it==goto_functions.function_map.end())
          throw "failed to find function `"+id2string(function_id)+"' in function map";

        // fix the type
        to_code_type(function_call.function().type()).return_type()=empty_typet();

        if(function_call.lhs().is_not_nil())
        {
          exprt rhs;
          
          symbol_exprt return_value;
          return_value.type()=function_call.lhs().type();
          return_value.set_identifier(id2string(function_id)+RETURN_VALUE_SUFFIX);
          rhs=return_value;

          goto_programt::targett t_a=goto_program.insert_after(i_it);
          t_a->make_assignment();
          t_a->source_location=i_it->source_location;
          t_a->code=code_assignt(function_call.lhs(), rhs);
          t_a->function=i_it->function;

          // fry the previous assignment
          function_call.lhs().make_nil();

          if(f_it->second.body_available())
          {
            goto_programt::targett t_d=goto_program.insert_after(t_a);
            t_d->make_dead();
            t_d->source_location=i_it->source_location;
            t_d->code=code_deadt(rhs);
            t_d->function=i_it->function;
          }
        }
      }
    }
  }

void show_symbol_table_plain(const namespacet &ns, std::ostream &out)
{
  out << std::endl << "Symbols:" << std::endl;
  out << "Number of symbols: " << ns.get_context().size() << std::endl;
  out << std::endl;

  ns.get_context().foreach_operand_in_order([&out, &ns](const symbolt &s) {
    int mode;

    if(s.mode == "")
      mode = 0;
    else
    {
      mode = get_mode(id2string(s.mode));
      if(mode < 0)
        throw "symbol " + id2string(s.name) + " has unknown mode";
    }

    std::unique_ptr<languaget> p(mode_table[mode].new_language());
    std::string type_str, value_str;

    if(s.type.is_not_nil())
      p->from_type(s.type, type_str, ns);

    if(s.value.is_not_nil())
      p->from_expr(s.value, value_str, ns);

    out << "Symbol......: " << s.name << std::endl;
    out << "Pretty name.: " << s.pretty_name << std::endl;
    out << "Module......: " << s.module << std::endl;
    out << "Base name...: " << s.base_name << std::endl;
    out << "Mode........: " << s.mode << " (" << mode << ")" << std::endl;
    out << "Type........: " << type_str << std::endl;
    out << "Value.......: " << value_str << std::endl;
    out << "Flags.......:";

    if(s.lvalue)
      out << " lvalue";
    if(s.static_lifetime)
      out << " static_lifetime";
    if(s.file_local)
      out << " file_local";
    if(s.is_type)
      out << " type";
    if(s.is_extern)
      out << " extern";
    if(s.is_macro)
      out << " macro";
    if(s.is_used)
      out << " used";

    out << std::endl;
    out << "Location....: " << s.location << std::endl;

    out << std::endl;
  });
}

void configt::set_from_symbol_table(
  const symbol_tablet &symbol_table)
{
  // maybe not compiled from C/C++
  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
     symbol_table.symbols.end())
    return;

  namespacet ns(symbol_table);
  
  // clear defines
  ansi_c.defines.clear();

  // first set architecture to get some defaults
  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
     symbol_table.symbols.end())
    set_arch(id2string(this_architecture()));
  else
    set_arch(string_from_ns(ns, "arch"));
  
  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
  ansi_c.bool_width=1*8;
  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");

  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
  ansi_c.use_fixed_for_float=unsigned_from_ns(ns, "fixed_for_float")!=0;
  // for_has_scope, single_precision_constant, rounding_mode not
  // stored in namespace

  ansi_c.alignment=unsigned_from_ns(ns, "alignment");

  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");

  ansi_c.endianness=(ansi_ct::endiannesst)unsigned_from_ns(ns, "endianness");

  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
     symbol_table.symbols.end())
    ansi_c.os=ansi_ct::string_to_os(id2string(this_operating_system()));
  else
    ansi_c.os=ansi_ct::string_to_os(id2string(string_from_ns(ns, "os")));

  //NULL_is_zero=from_ns("NULL_is_zero");
  ansi_c.NULL_is_zero=true;

  // mode, preprocessor (and all preprocessor command line options),
  // lib, string_abstraction not stored in namespace
}

void file_view(const datat &data)
{
  std::ofstream out("file_view.html");

  out << "<html>\n<head>\n";
  out << "<title>" << html_escape(data.description) << "</title>\n";
  
  out << "<style type=\"text/css\">\n";
  out << "/* Source-code listing */\n";
  out << "div.file { float: left; padding-right: 20px; }\n";
  out << "div.listing { font-size: 3px; width: 150px; height: 400px; overflow-y: scroll; overflow-x: scroll; white-space: pre; }\n";
  out << "div.filename { text-align: center; font-size: 14px; width: 150px; }\n";

  out << "strong.alarm { font-style: normal; background-color: #ff6633; font-weight: normal; }\n";
  
  out << "/* Description of sw under test */\n";
  out << "div.description { float: center; font: 14px \"Trebuchet MS\", Verdana, Arial, Helvetica, sans-serif;  width=100%; text-align: center; }\n";
  
  out << "</style>\n";
  out << "</head>\n";
  
  out << "<body>\n";
  
  out << "<center><img src=\"http://www.deltacheck.org/deltacheck_logo_small.png\"></center>\n";
  
  out << "<div class=\"description\">\n";
  out << html_escape(data.description) << "\n";
  out << "</div>\n";
  
  std::set<irep_idt> files;
  
  for(datat::propertiest::const_iterator
      e_it=data.properties.begin();
      e_it!=data.properties.end();
      e_it++)
    files.insert(e_it->file);

  for(std::set<irep_idt>::const_iterator
      f_it=files.begin();
      f_it!=files.end();
      f_it++)
  {
    if(has_prefix(id2string(*f_it), "/usr/include/"))
      continue;
  
    if(has_prefix(id2string(*f_it), "<builtin-library>"))
      continue;
  
    print_file(data, *f_it, out);
  }
  
  out << "</body>\n</html>\n";
}

void update_function_signature(
  const local_SSAt &SSA,
  class jsont &dest)
{
  jsont &j_signature=dest["signature"];
  jsont &j_reads=j_signature["reads"];
  jsont &j_modifies=j_signature["modifies"];

  j_signature.kind=jsont::J_OBJECT;
  j_reads=jsont::json_array();
  j_modifies=jsont::json_array();
  
  std::set<irep_idt> modifies;
  std::set<irep_idt> reads;

  for(assignmentst::assignment_mapt::const_iterator
      a_it=SSA.assignments.assignment_map.begin();
      a_it!=SSA.assignments.assignment_map.end();
      a_it++)
  {
    for(assignmentst::objectst::const_iterator
        o_it=a_it->second.begin();
        o_it!=a_it->second.end();
        o_it++)
    {
      modifies.insert(o_it->get_identifier());
    }
  }

  for(ssa_objectst::objectst::const_iterator
      o_it=SSA.ssa_objects.objects.begin();
      o_it!=SSA.ssa_objects.objects.end();
      o_it++)
  {
    reads.insert(o_it->get_identifier());
  }

  for(std::set<irep_idt>::const_iterator it=reads.begin();
      it!=reads.end();
      it++)
  {
    j_reads.array.push_back(jsont::json_string(id2string(*it)));
  }

  for(std::set<irep_idt>::const_iterator it=modifies.begin();
      it!=modifies.end();
      it++)
  {
    j_modifies.array.push_back(jsont::json_string(id2string(*it)));
  }

}