void remove_return(goto_programt &body, const goto_programt::targett pos)
{
  code_function_callt &call=to_code_function_call(pos->code);
  const irep_idt &id=to_symbol_expr(call.function()).get_identifier();
  const typet &type=call.lhs().type();
  const source_locationt &loc=pos->source_location;
  const irep_idt &func=pos->function;
  const goto_programt::targett assign=body.insert_after(pos);
  assign->make_assignment();
  assign->source_location=loc;
  assign->code=code_assignt(call.lhs(), get_ret_val_var(id, type));
  assign->function=func;
  call.lhs().make_nil();
}

void all_paths_enumeratort::extend_path(patht &path,
    goto_programt::targett t,
    int succ) {
  goto_programt::targett next;
  goto_programt::targetst succs;
  exprt guard = true_exprt();

  goto_program.get_successors(t, succs);

  for (goto_programt::targetst::iterator it = succs.begin();
       it != succs.end();
       ++it) {
    if (succ == 0) {
      next = *it;
      break;
    }

    succ--;
  }

  if (t->is_goto()) {
    guard = not_exprt(t->guard);

    for (goto_programt::targetst::iterator it = t->targets.begin();
         it != t->targets.end();
         ++it) {
      if (next == *it) {
        guard = t->guard;
        break;
      }
    }
  }

  path.push_back(path_nodet(next, guard));
}

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);
}

goto_programt::targett add_return_assignment(goto_programt &body,
    goto_programt::targett pos, const irep_idt &func_id, const exprt &value)
{
  const source_locationt &loc=pos->source_location;
  pos=body.insert_after(pos);
  pos->make_assignment();
  pos->source_location=loc;
  pos->code=code_assignt(get_ret_val_var(func_id, value.type()), value);
  return pos;
}

void acceleratet::make_overflow_loc(
  goto_programt::targett loop_header,
  goto_programt::targett &loop_end,
  goto_programt::targett &overflow_loc)
{
  symbolt overflow_sym=utils.fresh_symbol("accelerate::overflow", bool_typet());
  const exprt &overflow_var=overflow_sym.symbol_expr();
  natural_loops_mutablet::natural_loopt &loop =
    natural_loops.loop_map[loop_header];
  overflow_instrumentert instrumenter(program, overflow_var, symbol_table);

  for(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
      it!=loop.end();
      ++it)
  {
    overflow_locs[*it]=goto_programt::targetst();
    goto_programt::targetst &added=overflow_locs[*it];

    instrumenter.add_overflow_checks(*it, added);
    loop.insert(added.begin(), added.end());
  }

  goto_programt::targett t=program.insert_after(loop_header);
  t->make_assignment();
  t->code=code_assignt(overflow_var, false_exprt());
  t->swap(*loop_header);
  loop.insert(t);
  overflow_locs[loop_header].push_back(t);

  goto_programt::instructiont s(SKIP);
  overflow_loc=program.insert_after(loop_end);
  *overflow_loc=s;
  overflow_loc->swap(*loop_end);
  loop.insert(overflow_loc);

  goto_programt::instructiont g(GOTO);
  g.guard=not_exprt(overflow_var);
  g.targets.push_back(overflow_loc);
  goto_programt::targett t2=program.insert_after(loop_end);
  *t2=g;
  t2->swap(*loop_end);
  overflow_locs[overflow_loc].push_back(t2);
  loop.insert(t2);

  goto_programt::targett tmp=overflow_loc;
  overflow_loc=loop_end;
  loop_end=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 remove_virtual_functionst::remove_virtual_function(
  goto_programt &goto_program,
  goto_programt::targett target)
{
  const code_function_callt &code=
    to_code_function_call(target->code);

  const auto &vcall_source_loc=target->source_location;

  const exprt &function=code.function();
  assert(function.id()==ID_virtual_function);
  assert(!code.arguments().empty());

  functionst functions;
  get_functions(function, functions);

  if(functions.empty())
  {
    target->make_skip();
    return; // give up
  }

  // only one option?
  if(functions.size()==1)
  {
    assert(target->is_function_call());
    if(functions.begin()->symbol_expr==symbol_exprt())
      target->make_skip();
    else
      to_code_function_call(target->code).function()=
        functions.begin()->symbol_expr;
    return;
  }

  // the final target is a skip
  goto_programt final_skip;

  goto_programt::targett t_final=final_skip.add_instruction();
  t_final->source_location=vcall_source_loc;

  t_final->make_skip();

  // build the calls and gotos

  goto_programt new_code_calls;
  goto_programt new_code_gotos;

  exprt this_expr=code.arguments()[0];
  // If necessary, cast to the last candidate function to
  // get the object's clsid. By the structure of get_functions,
  // this is the parent of all other classes under consideration.
  const auto &base_classid=functions.back().class_id;
  const auto &base_function_symbol=functions.back().symbol_expr;
  symbol_typet suggested_type(base_classid);
  exprt c_id2=get_class_identifier_field(this_expr, suggested_type, ns);

  std::map<irep_idt, goto_programt::targett> calls;
  // Note backwards iteration, to get the least-derived candidate first.
  for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
  {
    const auto &fun=*it;
    auto insertit=calls.insert(
      {fun.symbol_expr.get_identifier(), goto_programt::targett()});

    // Only create one call sequence per possible target:
    if(insertit.second)
    {
      goto_programt::targett t1=new_code_calls.add_instruction();
      t1->source_location=vcall_source_loc;
      if(!fun.symbol_expr.get_identifier().empty())
      {
      // call function
        t1->make_function_call(code);
        auto &newcall=to_code_function_call(t1->code);
        newcall.function()=fun.symbol_expr;
        pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
        if(!type_eq(newcall.arguments()[0].type(), need_type, ns))
          newcall.arguments()[0].make_typecast(need_type);
      }
      else
      {
        // No definition for this type; shouldn't be possible...
        t1->make_assertion(false_exprt());
      }
      insertit.first->second=t1;
      // goto final
      goto_programt::targett t3=new_code_calls.add_instruction();
      t3->source_location=vcall_source_loc;
      t3->make_goto(t_final, true_exprt());
    }

    // If this calls the base function we just fall through.
    // Otherwise branch to the right call:
    if(fun.symbol_expr!=base_function_symbol)
    {
      exprt c_id1=constant_exprt(fun.class_id, string_typet());
      goto_programt::targett t4=new_code_gotos.add_instruction();
      t4->source_location=vcall_source_loc;
      t4->make_goto(insertit.first->second, equal_exprt(c_id1, c_id2));
    }
//.........这里部分代码省略.........

void remove_virtual_functionst::remove_virtual_function(
  goto_programt &goto_program,
  goto_programt::targett target)
{
  const code_function_callt &code=
    to_code_function_call(target->code);

  const exprt &function=code.function();
  assert(function.id()==ID_virtual_function);
  assert(!code.arguments().empty());
  
  functionst functions;
  get_functions(function, functions);
  
  if(functions.empty())
  {
    target->make_skip();
    return; // give up
  }

  // the final target is a skip
  goto_programt final_skip;

  goto_programt::targett t_final=final_skip.add_instruction();
  t_final->make_skip();
  
  // build the calls and gotos

  goto_programt new_code_calls;
  goto_programt new_code_gotos;

  for(functionst::const_iterator
      it=functions.begin();
      it!=functions.end();
      it++)
  {
    // call function
    goto_programt::targett t1=new_code_calls.add_instruction();
    t1->make_function_call(code);
    to_code_function_call(t1->code).function()=it->symbol_expr;
    
    // goto final
    goto_programt::targett t3=new_code_calls.add_instruction();
    t3->make_goto(t_final, true_exprt());

    exprt this_expr=code.arguments()[0];    
    if(this_expr.type().id()!=ID_pointer ||
       this_expr.type().id()!=ID_struct)
    {
      symbol_typet symbol_type(it->class_id);
      this_expr=typecast_exprt(this_expr, pointer_typet(symbol_type));
    }
    
    exprt deref=dereference_exprt(this_expr, this_expr.type().subtype());
    exprt c_id1=constant_exprt(it->class_id, string_typet());
    exprt c_id2=build_class_identifier(deref);
    
    goto_programt::targett t4=new_code_gotos.add_instruction();
    t4->make_goto(t1, equal_exprt(c_id1, c_id2));
  }

  goto_programt new_code;
  
  // patch them all together
  new_code.destructive_append(new_code_gotos);
  new_code.destructive_append(new_code_calls);
  new_code.destructive_append(final_skip);
  
  // set locations
  Forall_goto_program_instructions(it, new_code)
  {
    irep_idt property_class=it->source_location.get_property_class();
    irep_idt comment=it->source_location.get_comment();
    it->source_location=target->source_location;
    it->function=target->function;
    if(!property_class.empty()) it->source_location.set_property_class(property_class);
    if(!comment.empty()) it->source_location.set_comment(comment);
  }

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 goto_inlinet::expand_function_call(
  goto_programt &dest,
  goto_programt::targett &target,
  const exprt &lhs,
  const exprt &function,
  const exprt::operandst &arguments,
  const exprt &constrain,
  bool full)
{
  // look it up
  if(function.id()!="symbol")
  {
    err_location(function);
    throw "function_call expects symbol as function operand, "
          "but got `"+function.id_string()+"'";
  }
  
  const irep_idt &identifier=function.identifier();
  
  // see if we are already expanding it
  if(recursion_set.find(identifier)!=recursion_set.end())
  {
    if(!full)
    {
      target++;
      return; // simply ignore, we don't do full inlining, it's ok
    }

    // it's really recursive. Uh. Buh. Give up.
    err_location(function);
    warning("recursion is ignored");
    target->make_skip();
    
    target++;
    return;
  }

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

  if(m_it==goto_functions.function_map.end())
  {
    err_location(function);
    str << "failed to find function `" << identifier
        << "'";
    throw 0;
  }
  
  goto_functiont &f=m_it->second;

  // see if we need to inline this  
  if(!full)
  {
    if(!f.body_available ||
       (!f.is_inlined() && f.body.instructions.size() > smallfunc_limit))
    {
      target++;
      return;
    }
  }

  if(f.body_available)
  {
    inlined_funcs.insert(identifier.as_string());
    for (std::set<std::string>::const_iterator it2 = f.inlined_funcs.begin();
         it2 != f.inlined_funcs.end(); it2++) {
      inlined_funcs.insert(*it2);
    }

    recursion_sett::iterator recursion_it=
      recursion_set.insert(identifier).first;  
  
    goto_programt tmp2;
    tmp2.copy_from(f.body);
    
    assert(tmp2.instructions.back().is_end_function());
    tmp2.instructions.back().type=LOCATION;
    
    replace_return(tmp2, lhs, constrain);
    
    goto_programt tmp;
    parameter_assignments(tmp2.instructions.front().location, f.type, arguments, tmp);
    tmp.destructive_append(tmp2);
    
    // set local variables
    Forall_goto_program_instructions(it, tmp)
      it->local_variables.insert(target->local_variables.begin(),
                                 target->local_variables.end());

    if(f.type.hide())
    {
      const locationt &new_location=function.find_location();
    
      Forall_goto_program_instructions(it, tmp)
      {
        if(new_location.is_not_nil())
        {
          // can't just copy, e.g., due to comments field
          it->location.id(""); // not NIL
          it->location.set_file(new_location.get_file());
//.........这里部分代码省略.........

void goto_inlinet::expand_function_call(
  goto_programt &dest,
  goto_programt::targett &target,
  const exprt &lhs,
  const symbol_exprt &function,
  const exprt::operandst &arguments,
  const exprt &constrain,
  bool full)
{
  // look it up
  const irep_idt identifier=function.get_identifier();
  
  // we ignore certain calls
  if(identifier=="__CPROVER_cleanup" ||
     identifier=="__CPROVER_set_must" ||
     identifier=="__CPROVER_set_may" ||
     identifier=="__CPROVER_clear_must" ||
     identifier=="__CPROVER_clear_may" ||
     identifier=="__CPROVER_cover")
  {
    target++;
    return; // ignore
  }
  
  // see if we are already expanding it
  if(recursion_set.find(identifier)!=recursion_set.end())
  {
    if(!full)
    {
      target++;
      return; // simply ignore, we don't do full inlining, it's ok
    }

    // it's really recursive, and we need full inlining.
    // Uh. Buh. Give up.
    warning().source_location=function.find_source_location();
    warning() << "recursion is ignored" << eom;
    target->make_skip();
    
    target++;
    return;
  }

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

  if(m_it==goto_functions.function_map.end())
  {
    if(!full)
    {
      target++;
      return; // simply ignore, we don't do full inlining, it's ok
    }

    error().source_location=function.find_source_location();
    error() << "failed to find function `" << identifier << "'" << eom;
    throw 0;
  }
  
  const goto_functionst::goto_functiont &f=m_it->second;

  // see if we need to inline this  
  if(!full)
  {
    if(!f.body_available() ||
       (!f.is_inlined() && f.body.instructions.size() > smallfunc_limit))
    {
      target++;
      return;
    }
  }

  if(f.body_available())
  {
    recursion_set.insert(identifier);

    // first make sure that this one is already inlined
    goto_inline_rec(m_it, full);

    goto_programt tmp2;
    tmp2.copy_from(f.body);
    
    assert(tmp2.instructions.back().is_end_function());
    tmp2.instructions.back().type=LOCATION;
    
    replace_return(tmp2, lhs, constrain);

    goto_programt tmp;
    parameter_assignments(target->source_location, identifier, f.type, arguments, tmp);
    tmp.destructive_append(tmp2);
    parameter_destruction(target->source_location, identifier, f.type, tmp);

    if(f.is_hidden())
    {
      source_locationt new_source_location=
        function.find_source_location();
    
      if(new_source_location.is_not_nil())
      {
        new_source_location.set_hide();
//.........这里部分代码省略.........

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);
}