void local_SSAt::build_transfer(locationt loc)
{
  if(loc->is_assign())
  {
    const code_assignt &code_assign=to_code_assign(loc->code);

    exprt deref_lhs=dereference(code_assign.lhs(), loc);
    exprt deref_rhs=dereference(code_assign.rhs(), loc);

    assign_rec(deref_lhs, deref_rhs, true_exprt(), loc);
  }
  else if(loc->is_function_call())
  {
    const code_function_callt &code_function_call=
      to_code_function_call(loc->code);
      
    const exprt &lhs=code_function_call.lhs();
      
    if(lhs.is_not_nil())
    {
      exprt deref_lhs=dereference(lhs, loc);
    
      // generate a symbol for rhs
      irep_idt identifier="ssa::return_value"+i2string(loc->location_number);
      symbol_exprt rhs(identifier, code_function_call.lhs().type());
      
      assign_rec(deref_lhs, rhs, true_exprt(), loc);
    }
  }
}

  inline bool merge(
    const is_threaded_domaint &src,
    locationt from,
    locationt to)
  {
    bool old_reachable=reachable;
    if(src.reachable)
      reachable=true;

    bool old_h_s=has_spawn;
    if(src.has_spawn &&
       (from->is_end_function() ||
        from->function==to->function))
      has_spawn=true;

    bool old_i_t=is_threaded;
    if(has_spawn ||
       (src.is_threaded &&
       !from->is_end_function()))
      is_threaded=true;

    return old_reachable!=reachable ||
           old_i_t!=is_threaded ||
           old_h_s!=has_spawn;
  }

void local_SSAt::build_cond(locationt loc)
{
  // anything to be built?
  if(!loc->is_goto() &&
     !loc->is_assume()) return;
  
  // produce a symbol for the renamed branching condition
  equal_exprt equality(cond_symbol(loc), read_rhs(loc->guard, loc));
  nodes[loc].equalities.push_back(equality);
}

xmlt xml(const locationt &location)
{
  xmlt xml_location;
  xml_location.name="location";

  if(location.get_file()!="")
    xml_location.set_attribute("file", id2string(location.get_file()));
    
  if(location.get_line()!="")
    xml_location.set_attribute("line", id2string(location.get_line()));

  return xml_location;
}

 void transform(
   locationt from,
   locationt to,
   ai_baset &ai,
   const namespacet &ns) override final
 {
   if(!reachable) return;
   if(from->is_start_thread() ||
      to->is_end_thread())
   {
     has_spawn=true;
     is_threaded=true;
   }
 }

expr2tc abstract_domain_baset::get_return_lhs(locationt to) const
{
  // get predecessor of "to"

  to--;

  if(to->is_end_function())
    return expr2tc();
  
  // must be the function call
  assert(to->is_function_call());

  const code_function_call2t &code = to_code_function_call2t(to->code);
  
  return code.ret;
}

exprt flow_insensitive_abstract_domain_baset::get_return_lhs(locationt to) const
{
  // get predecessor of "to"

  to--;

  if(to->is_end_function())
    return static_cast<const exprt &>(get_nil_irep());

  // must be the function call
  assert(to->is_function_call());

  const code_function_callt &code=
    to_code_function_call(to_code(to->code));

  return code.lhs();
}

exprt local_SSAt::edge_guard(locationt from, locationt to) const
{
  if(from->is_goto())
  {
    // big question: taken or not taken?
    if(to==from->get_target())
      return and_exprt(guard_symbol(from), cond_symbol(from));
    else
      return and_exprt(guard_symbol(from), not_exprt(cond_symbol(from)));
  }
  else if(from->is_assume())
  {
    return and_exprt(guard_symbol(from), cond_symbol(from));
  }
  else
    return guard_symbol(from);
}

void local_SSAt::build_assertions(locationt loc)
{
  if(loc->is_assert())
  {
    exprt c=read_rhs(loc->guard, loc);
    exprt g=guard_symbol(loc);    
    nodes[loc].assertion=implies_exprt(g, c);
  }
}

  void transform(
    locationt from,
    locationt to,
    ai_baset &ai,
    const namespacet &ns) final
  {
    // assert(reachable);

    if(!reachable)
      return;

    if(from->is_start_thread())
      is_threaded=true;
  }

void message_handlert::print(
  unsigned level,
  const std::string &message,
  int sequence_number,
  const locationt &location)
{
  std::string dest;
  
  const irep_idt &file=location.get_file();
  const irep_idt &line=location.get_line();
  const irep_idt &column=location.get_column();
  const irep_idt &function=location.get_function();

  if(file!="")     { if(dest!="") dest+=" "; dest+="file "+id2string(file); }
  if(line!="")     { if(dest!="") dest+=" "; dest+="line "+id2string(line); }
  if(column!="")   { if(dest!="") dest+=" "; dest+="column "+id2string(column); }
  if(function!="") { if(dest!="") dest+=" "; dest+="function "+id2string(function); }

  if(dest!="") dest+=": ";
  dest+=message;

  print(level, dest);
}

xmlt xml(const locationt &location)
{
  xmlt result;

  result.name="location";
  
  // these will go away
  result.new_element("file").data=id2string(location.get_file());
  result.new_element("line").data=id2string(location.get_line());
  result.new_element("function").data=id2string(location.get_function());
  
  // these are to stay
  if(location.get_file()!="")
    result.set_attribute("file", id2string(location.get_file()));

  if(location.get_line()!="")
    result.set_attribute("line", id2string(location.get_line()));

  if(location.get_function()!="")
    result.set_attribute("function", id2string(location.get_function()));
  
  return result;
}

expr2tc abstract_domain_baset::get_guard(
  locationt from,
  locationt to) const
{
  if(!from->is_goto())
    return true_expr;

  locationt next=from;
  next++;

  if(next==to)
  {
    expr2tc tmp = not2tc(from->guard);
    return tmp;
  }
  
  return from->guard;
}

exprt flow_insensitive_abstract_domain_baset::get_guard(
  locationt from,
  locationt to) const
{
  if(!from->is_goto())
    return true_exprt();

  locationt next=from;
  next++;

  if(next==to)
  {
    exprt tmp(from->guard);
    tmp.make_not();
    return tmp;
  }

  return from->guard;
}

void document_claimst::get_code(
  const locationt &location,
  std::string &dest)
{
  dest="";

  const irep_idt &file=location.get_file();
  const irep_idt &line=location.get_line();

  if(file=="" || line=="") return;

  std::ifstream in(file.c_str());

  if(!in)
  {
    dest+="ERROR: unable to open ";
    dest+=id2string(file);
    dest+="\n";
    return;
  }

  int line_int=atoi(line.c_str());

  int line_start=line_int-3,
      line_end=line_int+3;

  if(line_start<=1) line_start=1;

  // skip line_start-1 lines

  for(int l=0; l<line_start-1; l++)
  {
    std::string tmp;
    std::getline(in, tmp);
  }

  // read till line_end

  std::list<linet> lines;

  for(int l=line_start; l<=line_end && in; l++)
  {
    lines.push_back(linet());

    std::string &line=lines.back().text;
    std::getline(in, line);

    if(!line.empty() && line[line.size()-1]=='\r')
      line.resize(line.size()-1);

    lines.back().line_number=l;
  }

  // remove empty lines at the end and at the beginning

  for(std::list<linet>::iterator it=lines.begin();
      it!=lines.end();)
  {
    if(is_empty(it->text))
      it=lines.erase(it);
    else
      break;
  }    

  for(std::list<linet>::iterator it=lines.end();
      it!=lines.begin();)
  {
    it--;

    if(is_empty(it->text))
      it=lines.erase(it);
    else
      break;
  }

  // strip space
  strip_space(lines);

  // build dest

  for(std::list<linet>::iterator it=lines.begin();
      it!=lines.end(); it++)
  {
    std::string line_no=i2string(it->line_number);

    std::string tmp;

    switch(format)
    {
    case LATEX:
      while(line_no.size()<4)
        line_no=" "+line_no;
    
      line_no+"  ";
    
      tmp+=escape_latex(it->text, true);

      if(it->line_number==line_int)
        tmp="{\\ttb{}"+tmp+"}";
        
//.........这里部分代码省略.........

void goto_inlinet::parameter_assignments(
  const locationt &location,
  const code_typet &code_type,
  const exprt::operandst &arguments,
  goto_programt &dest)
{
  // iterates over the operands
  exprt::operandst::const_iterator it1=arguments.begin();

  goto_programt::local_variablest local_variables;
  
  const code_typet::argumentst &argument_types=
    code_type.arguments();
  
  // iterates over the types of the arguments
  for(code_typet::argumentst::const_iterator
      it2=argument_types.begin();
      it2!=argument_types.end();
      it2++)
  {
    // if you run out of actual arguments there was a mismatch
    if(it1==arguments.end())
    {
      err_location(location);
      throw "function call: not enough arguments";
    }

    const exprt &argument=static_cast<const exprt &>(*it2);

    // this is the type the n-th argument should be
    const typet &arg_type=ns.follow(argument.type());

    const irep_idt &identifier=argument.cmt_identifier();

    if(identifier=="")
    {
      err_location(location);
      throw "no identifier for function argument";
    }

    {
      const symbolt &symbol=ns.lookup(identifier);

      goto_programt::targett decl=dest.add_instruction();
      decl->make_other();
      exprt tmp = code_declt(symbol_expr(symbol));
      migrate_expr(tmp, decl->code);
      decl->location=location;
      decl->function=location.get_function(); 
      decl->local_variables=local_variables;
    }

    local_variables.insert(identifier);
    
    // nil means "don't assign"
    if(it1->is_nil())
    {    
    }
    else
    {
      // this is the actual parameter
      exprt actual(*it1);

      // it should be the same exact type
      type2tc arg_type_2, actual_type_2;
      migrate_type(arg_type, arg_type_2);
      migrate_type(actual.type(), actual_type_2);
      if (!base_type_eq(arg_type_2, actual_type_2, ns))
      {
        const typet &f_argtype = ns.follow(arg_type);
        const typet &f_acttype = ns.follow(actual.type());
        
        // we are willing to do some conversion
        if((f_argtype.id()=="pointer" &&
            f_acttype.id()=="pointer") ||
           (f_argtype.is_array() &&
            f_acttype.id()=="pointer" &&
            f_argtype.subtype()==f_acttype.subtype()))
        {
          actual.make_typecast(arg_type);
        }
        else if((f_argtype.id()=="signedbv" ||
            f_argtype.id()=="unsignedbv" ||
            f_argtype.is_bool()) &&
           (f_acttype.id()=="signedbv" ||
            f_acttype.id()=="unsignedbv" ||
            f_acttype.is_bool()))  
        {
          actual.make_typecast(arg_type);
        }
        else
        {
          err_location(location);

          str << "function call: argument `" << identifier
              << "' type mismatch: got "
              << from_type(ns, identifier, it1->type())
              << ", expected "
              << from_type(ns, identifier, arg_type);
          throw 0;
//.........这里部分代码省略.........

void ssa_domaint::transform(
  locationt from,
  locationt to,
  ai_baset &ai,
  const namespacet &ns)
{
  if(from->is_assign() || from->is_decl() || from->is_function_call())
  {
    const auto &assignments=static_cast<ssa_ait &>(ai).assignments;
    const std::set<ssa_objectt> &assigns=assignments.get(from);

    for(std::set<ssa_objectt>::const_iterator
        o_it=assigns.begin();
        o_it!=assigns.end();
        o_it++)
    {
      if(o_it->get_expr().get_bool("#is_rhs_assign") &&
         is_pointed(o_it->get_root_object()))
      {
        // the second part excluded cases
        // when a result of malloc is at the right-handed side
        const auto object_ai_it=
          static_cast<ssa_ait &>(ai)[from].def_map.find(o_it->get_identifier());
        if(object_ai_it!=static_cast<ssa_ait &>(ai)[from].def_map.end() &&
           object_ai_it->second.def.is_assignment())
        {
          const exprt pointer=
            get_pointer(
              o_it->get_root_object(),
              pointed_level(o_it->get_root_object())-1);
          const auto def_pointer=
            static_cast<ssa_ait &>(ai)[from]
              .def_map.find(
                ssa_objectt(pointer, ns).get_identifier())->second.def;
          if(!def_pointer.is_assignment() ||
             def_pointer.loc->location_number<
               object_ai_it->second.def.loc->location_number)
          {
            continue;
          }
        }
      }
      irep_idt identifier=o_it->get_identifier();

      def_entryt &def_entry=def_map[identifier];
      def_entry.def.loc=from;
      def_entry.source=from;
      auto guard_it=assignments.alloc_guards_map.find({from, *o_it});
      if(guard_it!=assignments.alloc_guards_map.end())
      {
        def_entry.def.kind=deft::ALLOCATION;
        def_entry.def.guard=guard_it->second;
      }
      else
        def_entry.def.kind=deft::ASSIGNMENT;
    }
  }
  else if(from->is_dead())
  {
    const code_deadt &code_dead=to_code_dead(from->code);
    const irep_idt &id=code_dead.get_identifier();
    def_map.erase(id);
  }

  // update source in all defs
  for(def_mapt::iterator
      d_it=def_map.begin(); d_it!=def_map.end(); d_it++)
    d_it->second.source=from;
}

void rd_range_domaint::transform(
  locationt from,
  locationt to,
  ai_baset &ai,
  const namespacet &ns)
{
  reaching_definitions_analysist *rd=
    dynamic_cast<reaching_definitions_analysist*>(&ai);
  assert(rd!=0);

  assert(bv_container);

  // kill values
  if(from->is_dead())
    transform_dead(ns, from);
  // kill thread-local values
  else if(from->is_start_thread())
    transform_start_thread(ns, *rd);
  // do argument-to-parameter assignments
  else if(from->is_function_call())
    transform_function_call(ns, from, to, *rd);
  // cleanup parameters
  else if(from->is_end_function())
    transform_end_function(ns, from, to, *rd);
  // lhs assignements
  else if(from->is_assign())
    transform_assign(ns, from, from, *rd);
  // initial (non-deterministic) value
  else if(from->is_decl())
    transform_assign(ns, from, from, *rd);

#if 0
  // handle return values
  if(to->is_function_call())
  {
    const code_function_callt &code=to_code_function_call(to->code);

    if(code.lhs().is_not_nil())
    {
      rw_range_set_value_sett rw_set(ns, rd->get_value_sets());
      goto_rw(to, rw_set);
      const bool is_must_alias=rw_set.get_w_set().size()==1;

      forall_rw_range_set_w_objects(it, rw_set)
      {
        const irep_idt &identifier=it->first;
        // ignore symex::invalid_object
        const symbolt *symbol_ptr;
        if(ns.lookup(identifier, symbol_ptr))
          continue;
        assert(symbol_ptr!=0);

        const range_domaint &ranges=rw_set.get_ranges(it);

        if(is_must_alias &&
           (!rd->get_is_threaded()(from) ||
            (!symbol_ptr->is_shared() &&
             !rd->get_is_dirty()(identifier))))
          for(const auto &range : ranges)
            kill(identifier, range.first, range.second);
      }
    }
  }