void string_instrumentationt::do_fscanf(
  goto_programt &dest,
  goto_programt::targett target,
  code_function_callt &call)
{
  const code_function_callt::argumentst &arguments=call.arguments();
  
  if(arguments.size()<2)
  {
    err_location(target->location);
    throw "fscanf expected to have two or more arguments";
  }
  
  goto_programt tmp;
  
  do_format_string_write(tmp, target, arguments, 1, 2, "fscanf");
  
  if(call.lhs().is_not_nil())
  {
    goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
    return_assignment->location=target->location;
      
    exprt rhs=side_effect_expr_nondett(call.lhs().type());
    rhs.location()=target->location;
      
    return_assignment->code=code_assignt(call.lhs(), rhs);
  }
  
  target->make_skip();
  dest.insert_before_swap(target, tmp);
}

void goto_convertt::convert_function_call(
  const code_function_callt &function_call,
  goto_programt &dest)
{
  do_function_call(
    function_call.lhs(),
    function_call.function(),
    function_call.arguments(),
    dest);
}

void string_instrumentationt::do_strtok(
  goto_programt &dest,
  goto_programt::targett target,
  code_function_callt &call)
{
  const code_function_callt::argumentst &arguments=call.arguments();

  if(arguments.size()!=2)
  {
    err_location(target->location);
    throw "strtok expected to have two arguments";
  }
  
  goto_programt tmp;

  goto_programt::targett assertion0=tmp.add_instruction();
  assertion0->make_assertion(is_zero_string(arguments[0]));
  assertion0->location=target->location;
  assertion0->location.set("property", "string");
  assertion0->location.set("comment", "zero-termination of 1st string argument of strtok");

  goto_programt::targett assertion1=tmp.add_instruction();
  assertion1->make_assertion(is_zero_string(arguments[1]));
  assertion1->location=target->location;
  assertion1->location.set("property", "string");
  assertion1->location.set("comment", "zero-termination of 2nd string argument of strtok");

  target->make_skip();
  dest.insert_before_swap(target, tmp);
}

void string_instrumentationt::do_strstr(
  goto_programt &dest,
  goto_programt::targett target,
  code_function_callt &call)
{
  const code_function_callt::argumentst &arguments=call.arguments();

  if(arguments.size()!=2)
  {
    error().source_location=target->source_location;
    error() << "strstr expected to have two arguments" << eom;
    throw 0;
  }
  
  goto_programt tmp;

  goto_programt::targett assertion0=tmp.add_instruction();
  assertion0->make_assertion(is_zero_string(arguments[0]));
  assertion0->source_location=target->source_location;
  assertion0->source_location.set_property_class("string");
  assertion0->source_location.set_comment("zero-termination of 1st string argument of strstr");

  goto_programt::targett assertion1=tmp.add_instruction();
  assertion1->make_assertion(is_zero_string(arguments[1]));
  assertion1->source_location=target->source_location;
  assertion1->source_location.set_property_class("string");
  assertion1->source_location.set_comment("zero-termination of 2nd string argument of strstr");

  target->make_skip();
  dest.insert_before_swap(target, tmp);
}

void string_instrumentationt::do_snprintf(
  goto_programt &dest,
  goto_programt::targett target,
  code_function_callt &call)
{
  const code_function_callt::argumentst &arguments=call.arguments();

  if(arguments.size()<3)
  {
    error().source_location=target->source_location;
    error() << "snprintf expected to have three or more arguments"
            << eom;
    throw 0;
  }

  goto_programt tmp;

  goto_programt::targett assertion=tmp.add_instruction();
  assertion->source_location=target->source_location;
  assertion->source_location.set_property_class("string");
  assertion->source_location.set_comment("snprintf buffer overflow");

  exprt bufsize=buffer_size(arguments[0]);
  assertion->make_assertion(
    binary_relation_exprt(bufsize, ID_ge, arguments[1]));

  do_format_string_read(tmp, target, arguments, 2, 3, "snprintf");

  if(call.lhs().is_not_nil())
  {
    goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
    return_assignment->source_location=target->source_location;

    exprt rhs=side_effect_expr_nondett(call.lhs().type());
    rhs.add_source_location()=target->source_location;

    return_assignment->code=code_assignt(call.lhs(), rhs);
  }

  target->make_skip();
  dest.insert_before_swap(target, tmp);
}

void string_instrumentationt::do_sprintf(
  goto_programt &dest,
  goto_programt::targett target,
  code_function_callt &call)
{
  const code_function_callt::argumentst &arguments=call.arguments();
    
  if(arguments.size()<2)
  {
    error().source_location=target->source_location;
    error() << "sprintf expected to have two or more arguments" << eom;
    throw 0;
  }
  
  goto_programt tmp;
  
  goto_programt::targett assertion=tmp.add_instruction();  
  assertion->source_location=target->source_location;
  assertion->source_location.set_property_class("string");  
  assertion->source_location.set_comment("sprintf buffer overflow");
  
  // in the abstract model, we have to report a 
  // (possibly false) positive here
  assertion->make_assertion(false_exprt());
  
  do_format_string_read(tmp, target, arguments, 1, 2, "sprintf");
  
  if(call.lhs().is_not_nil())
  {
    goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
    return_assignment->source_location=target->source_location;
    
    exprt rhs=side_effect_expr_nondett(call.lhs().type());
    rhs.add_source_location()=target->source_location;
      
    return_assignment->code=code_assignt(call.lhs(), rhs);
  }
  
  target->make_skip();
  dest.insert_before_swap(target, tmp);
}

void remove_function_pointerst::fix_return_type(
  code_function_callt &function_call,
  goto_programt &dest)
{  
  // are we returning anything at all?
  if(function_call.lhs().is_nil()) return;
  
  const code_typet &code_type=
    to_code_type(ns.follow(function_call.function().type()));
  
  // type already ok?
  if(type_eq(
       function_call.lhs().type(),
       code_type.return_type(), ns))
    return;

  symbolt &tmp_symbol=new_tmp_symbol();
  tmp_symbol.type=code_type.return_type();
  tmp_symbol.location=function_call.location();

  symbol_exprt tmp_symbol_expr;
  tmp_symbol_expr.type()=tmp_symbol.type;
  tmp_symbol_expr.set_identifier(tmp_symbol.name);
  
  exprt old_lhs=function_call.lhs();
  function_call.lhs()=tmp_symbol_expr;

  goto_programt::targett t_assign=dest.add_instruction();
  t_assign->make_assignment();
  t_assign->code=code_assignt(
    old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()));
}  

void remove_function_pointerst::fix_argument_types(
  code_function_callt &function_call)
{
  const code_typet &code_type=
    to_code_type(ns.follow(function_call.function().type()));

  const code_typet::parameterst &function_parameters=
    code_type.parameters();

  code_function_callt::argumentst &call_arguments=
    function_call.arguments();

  for(unsigned i=0; i<function_parameters.size(); i++)
  {
    if(i<call_arguments.size())
    {
      if(!type_eq(call_arguments[i].type(),
                  function_parameters[i].type(), ns))
      {
        call_arguments[i].make_typecast(function_parameters[i].type());
      }
    }
  }
}

void termination_baset::find_required_steps(
  const goto_tracet &goto_trace,
  goto_tracet::stepst::const_iterator &loop_begin,
  required_stepst &required_steps,
  const std::string &prefix) const
{
  find_symbols_sett required_symbols;
  unsigned before=0, after=1;

  // initialize: find all (potential) loop exits and
  // remember the symbols in them
  for(goto_tracet::stepst::const_iterator it1=loop_begin;
      it1!=goto_trace.steps.end();
      it1++)
  {
    if(it1->pc->is_goto() &&
       it1->pc->function==loop_begin->pc->function)
    {
      bool found_next=false, found_target=false;
      goto_programt::const_targett next=it1->pc; next++;
      goto_programt::const_targett target=it1->pc->targets.front();

      for(goto_tracet::stepst::const_iterator it2=loop_begin;
          it2!=goto_trace.steps.end();
          it2++)
      {
        if(it1!=it2)
        {
          if(it2->pc==next)
            found_next=true;
          else if(it2->pc==target)
            found_target=true;
        }
      }

      if(!found_target || !found_next)
      {
        exprt temp=it1->cond_expr;
        remove_ssa_ids(temp);
        find_symbols(temp, required_symbols);
      }
    }
  }

  #if 0
  std::cout << "INITIAL SYMBOLS: ";
  for(find_symbols_sett::const_iterator it=required_symbols.begin();
      it!=required_symbols.end();
      it++)
    std::cout << *it << ", ";
  std::cout << std::endl;
  #endif

  // get the fixpoint
  while(before!=after)
  {
    before=required_symbols.size();

    for(goto_tracet::stepst::const_iterator step=loop_begin;
        step!=goto_trace.steps.end();
        step++)
    {
      find_symbols_sett intersection;

      if(step->is_assignment())
      {
        exprt lhs, rhs;

        const codet &code=to_code(step->pc->code);

        if(code.get_statement()==ID_assign)
        {
          const code_assignt &acode=to_code_assign(step->pc->code);
          lhs=acode.lhs();
          rhs=acode.rhs();
        }
        else if(code.get_statement()==ID_function_call)
        {
          const code_function_callt fcode=to_code_function_call(step->pc->code);
          lhs=fcode.lhs();
          rhs=fcode.op2();
        }
        else
          throw "Unexpected assign statement";

        if(lhs.id()==ID_symbol &&
           has_prefix(lhs.get_string(ID_identifier), prefix))
        {
          // if we depend on the RHS syms, we also need the pre-symbol
          find_symbols_sett rhs_sym;
          find_symbols(rhs, rhs_sym);

          if(intersects(rhs_sym, required_symbols))
          {
            find_symbols(lhs, required_symbols);
            required_steps.insert(&(*step));
          }
        }
        else
        {
//.........这里部分代码省略.........

std::string expr2javat::convert_code_function_call(
  const code_function_callt &src,
  unsigned indent)
{
  if(src.operands().size()!=3)
  {
    unsigned precedence;
    return convert_norep(src, precedence);
  }

  std::string dest=indent_str(indent);

  if(src.lhs().is_not_nil())
  {
    unsigned p;
    std::string lhs_str=convert(src.lhs(), p);

    // TODO: ggf. Klammern je nach p
    dest+=lhs_str;
    dest+='=';
  }

  const code_typet &code_type=
    to_code_type(src.function().type());

  bool has_this=code_type.has_this() &&
                !src.arguments().empty();

  if(has_this)
  {
    unsigned p;
    std::string this_str=convert(src.arguments()[0], p);
    dest+=this_str;
    dest+=" . "; // extra spaces for readability
  }

  {
    unsigned p;
    std::string function_str=convert(src.function(), p);
    dest+=function_str;
  }

  dest+='(';

  const exprt::operandst &arguments=src.arguments();

  bool first=true;

  forall_expr(it, arguments)
  {
    if(has_this && it==arguments.begin())
    {
    }
    else
    {
      unsigned p;
      std::string arg_str=convert(*it, p);

      if(first) first=false; else dest+=", ";
      // TODO: ggf. Klammern je nach p
      dest+=arg_str;
    }
  }

  dest+=");";

  return dest;
}

void jsil_typecheckt::typecheck_function_call(
  code_function_callt &call)
{
  if(call.operands().size()!=3)
    throw "function call expected to have three operands";

  exprt &lhs=call.lhs();
  typecheck_expr(lhs);

  exprt &f=call.function();
  typecheck_expr(f);

  for(auto &arg : call.arguments())
    typecheck_expr(arg);

  // Look for a function declaration symbol in the symbol table
  if(f.id()==ID_symbol)
  {
    const irep_idt &id=to_symbol_expr(f).get_identifier();

    if(symbol_table.has_symbol(id))
    {
      symbolt &s=symbol_table.lookup(id);

      if(s.type.id()==ID_code)
      {
        code_typet &codet=to_code_type(s.type);

        for(std::size_t i=0; i<codet.parameters().size(); i++)
        {
          if(i>=call.arguments().size()) break;

          const typet &param_type=codet.parameters()[i].type();

          if(!param_type.id().empty() && param_type.is_not_nil())
          {
             // check argument's type if parameter's type is given
             make_type_compatible(call.arguments()[i], param_type, true);
          }
        }

        // if there are too few arguments, add undefined
        if(codet.parameters().size()>call.arguments().size())
        {
          for(std::size_t i=call.arguments().size();
              i<codet.parameters().size();
              ++i)
            call.arguments().push_back(
              exprt("undefined", jsil_undefined_type()));
        }

        // if there are too many arguments, remove
        while(codet.parameters().size()<call.arguments().size())
          call.arguments().pop_back();

        // check return type if exists
        if(!codet.return_type().id().empty() &&
            codet.return_type().is_not_nil())
          make_type_compatible(lhs, codet.return_type(), true);
        else make_type_compatible(lhs, jsil_any_type(), true);
      }
      else
      {
        // TODO: a symbol can be a variable evaluating to a string
        // which corresponds to a function identifier
        make_type_compatible(lhs, jsil_any_type(), true);
      }
    }
    else
    {
      // Should be function, declaration not found yet
      symbolt new_symbol;
      new_symbol.name=id;
      new_symbol.type=code_typet();
      new_symbol.mode="jsil";
      new_symbol.is_type=false;
      new_symbol.value=exprt("no-body-just-yet");

      make_type_compatible(lhs, jsil_any_type(), true);

      if(symbol_table.add(new_symbol))
        throw "failed to add expression symbol to symbol table";
    }
  }
  else
  {
    // TODO: this might be a string literal
    // which corresponds to a function identifier
    make_type_compatible(lhs, jsil_any_type(), true);
  }
}

void string_instrumentationt::do_strerror(
  goto_programt &dest,
  goto_programt::targett it,
  code_function_callt &call)
{
  if(call.lhs().is_nil())
  {
    it->make_skip();
    return;
  }

  irep_idt identifier_buf="c::__strerror_buffer";
  irep_idt identifier_size="c::__strerror_buffer_size";

  if(context.symbols.find(identifier_buf)==context.symbols.end())
  {
    symbolt new_symbol_size;
    new_symbol_size.base_name="__strerror_buffer_size";
    new_symbol_size.pretty_name=new_symbol_size.base_name;
    new_symbol_size.name=identifier_size;
    new_symbol_size.mode="C";
    new_symbol_size.type=uint_type();
    new_symbol_size.is_statevar=true;
    new_symbol_size.lvalue=true;
    new_symbol_size.static_lifetime=true;

    array_typet type;
    type.subtype()=char_type();
    type.size()=symbol_expr(new_symbol_size);
    symbolt new_symbol_buf;
    new_symbol_buf.mode="C";
    new_symbol_buf.type=type;
    new_symbol_buf.is_statevar=true;
    new_symbol_buf.lvalue=true;
    new_symbol_buf.static_lifetime=true;
    new_symbol_buf.base_name="__strerror_buffer";
    new_symbol_buf.pretty_name=new_symbol_buf.base_name;
    new_symbol_buf.name="c::"+id2string(new_symbol_buf.base_name);

    context.move(new_symbol_buf);
    context.move(new_symbol_size);
  }

  const symbolt &symbol_size=ns.lookup(identifier_size);
  const symbolt &symbol_buf=ns.lookup(identifier_buf);

  goto_programt tmp;

  {  
    goto_programt::targett assignment1=tmp.add_instruction(ASSIGN);
    exprt nondet_size=side_effect_expr_nondett(uint_type());

    assignment1->code=code_assignt(symbol_expr(symbol_size), nondet_size);
    assignment1->location=it->location;
    
    goto_programt::targett assumption1=tmp.add_instruction();

    assumption1->make_assumption(binary_relation_exprt(
      symbol_expr(symbol_size), "notequal",
      gen_zero(symbol_size.type)));

    assumption1->location=it->location;
  }

  // return a pointer to some magic buffer
  exprt index=exprt("index", char_type());
  index.copy_to_operands(symbol_expr(symbol_buf), gen_zero(uint_type()));

  exprt ptr=exprt("address_of", pointer_typet());
  ptr.type().subtype()=char_type();
  ptr.copy_to_operands(index);

  // make that zero-terminated
  {
    goto_programt::targett assignment2=tmp.add_instruction(ASSIGN);
    assignment2->code=code_assignt(is_zero_string(ptr, true), true_exprt());
    assignment2->location=it->location;
  }

  // assign address
  {
    goto_programt::targett assignment3=tmp.add_instruction(ASSIGN);
    exprt rhs=ptr;
    make_type(rhs, call.lhs().type());
    assignment3->code=code_assignt(call.lhs(), rhs);
    assignment3->location=it->location;
  }

  it->make_skip();
  dest.insert_before_swap(it, tmp);
}

void string_instrumentationt::do_strerror(
  goto_programt &dest,
  goto_programt::targett it,
  code_function_callt &call)
{
  if(call.lhs().is_nil())
  {
    it->make_skip();
    return;
  }

  irep_idt identifier_buf="__strerror_buffer";
  irep_idt identifier_size="__strerror_buffer_size";

  if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end())
  {
    symbolt new_symbol_size;
    new_symbol_size.base_name="__strerror_buffer_size";
    new_symbol_size.pretty_name=new_symbol_size.base_name;
    new_symbol_size.name=identifier_size;
    new_symbol_size.mode=ID_C;
    new_symbol_size.type=size_type();
    new_symbol_size.is_state_var=true;
    new_symbol_size.is_lvalue=true;
    new_symbol_size.is_static_lifetime=true;

    array_typet type;
    type.subtype()=char_type();
    type.size()=new_symbol_size.symbol_expr();
    symbolt new_symbol_buf;
    new_symbol_buf.mode=ID_C;
    new_symbol_buf.type=type;
    new_symbol_buf.is_state_var=true;
    new_symbol_buf.is_lvalue=true;
    new_symbol_buf.is_static_lifetime=true;
    new_symbol_buf.base_name="__strerror_buffer";
    new_symbol_buf.pretty_name=new_symbol_buf.base_name;
    new_symbol_buf.name=new_symbol_buf.base_name;

    symbol_table.move(new_symbol_buf);
    symbol_table.move(new_symbol_size);
  }

  const symbolt &symbol_size=ns.lookup(identifier_size);
  const symbolt &symbol_buf=ns.lookup(identifier_buf);

  goto_programt tmp;

  {
    goto_programt::targett assignment1=tmp.add_instruction(ASSIGN);
    exprt nondet_size=side_effect_expr_nondett(size_type());

    assignment1->code=code_assignt(symbol_size.symbol_expr(), nondet_size);
    assignment1->source_location=it->source_location;

    goto_programt::targett assumption1=tmp.add_instruction();

    assumption1->make_assumption(
      binary_relation_exprt(
        symbol_size.symbol_expr(),
        ID_notequal,
        from_integer(0, symbol_size.type)));

    assumption1->source_location=it->source_location;
  }

  // return a pointer to some magic buffer
  index_exprt index(
    symbol_buf.symbol_expr(),
    from_integer(0, index_type()),
    char_type());

  address_of_exprt ptr(index);

  // make that zero-terminated
  {
    goto_programt::targett assignment2=tmp.add_instruction(ASSIGN);
    assignment2->code=code_assignt(is_zero_string(ptr, true), true_exprt());
    assignment2->source_location=it->source_location;
  }

  // assign address
  {
    goto_programt::targett assignment3=tmp.add_instruction(ASSIGN);
    exprt rhs=ptr;
    make_type(rhs, call.lhs().type());
    assignment3->code=code_assignt(call.lhs(), rhs);
    assignment3->source_location=it->source_location;
  }

  it->make_skip();
  dest.insert_before_swap(it, tmp);
}