自学教程：C++ to_array_type函数代码示例

void c_typecheck_baset::designator_enter(  const typet &type,  designatort &designator){  designatort::entryt entry;  entry.type=type;  assert(entry.type.id()!=ID_symbol);    if(entry.type.id()==ID_struct)  {    entry.size=to_struct_type(entry.type).components().size();    if(entry.size!=0)      entry.subtype=to_struct_type(entry.type).components().front().type();    else      entry.subtype.make_nil();  }  else if(entry.type.id()==ID_union)  {    if(to_union_type(entry.type).components().empty())    {      entry.size=0;      entry.subtype.make_nil();    }    else    {      entry.size=1;      entry.subtype=to_union_type(entry.type).components().front().type();    }  }  else if(entry.type.id()==ID_array)  {    mp_integer array_size;    if(to_integer(to_array_type(entry.type).size(), array_size))    {      err_location(to_array_type(entry.type).size());      str << "array has non-constant size `"          << to_string(to_array_type(entry.type).size()) << "'";      throw 0;    }    entry.size=integer2long(array_size);    entry.subtype=entry.type.subtype();  }  else if(entry.type.id()==ID_incomplete_array)  {    entry.size=0;    entry.subtype=entry.type.subtype();  }  else    assert(false);  designator.push_entry(entry);}

smt_astt array_sym_smt_ast::select(smt_convt *ctx, const expr2tc &idx) const{  const array_type2t &array_type = to_array_type(sort->get_tuple_type());  const struct_union_data &data = ctx->get_type_def(array_type.subtype);  smt_sortt result_sort = ctx->convert_sort(array_type.subtype);  std::string name = ctx->mk_fresh_name("tuple_array_select::") + ".";  tuple_sym_smt_astt result = new tuple_sym_smt_ast(ctx, result_sort, name);  unsigned int i = 0;  for(auto const &it : data.members)  {    type2tc arrtype(      new array_type2t(it, array_type.array_size, array_type.size_is_infinite));    smt_astt result_field = result->project(ctx, i);    smt_astt sub_array = project(ctx, i);    smt_astt selected = sub_array->select(ctx, idx);    ctx->assert_ast(result_field->eq(ctx, selected));    i++;  }  return result;}

void c_typecheck_baset::do_initializer(  exprt &initializer,  const typet &type,  bool force_constant){  exprt result=do_initializer_rec(initializer, type, force_constant);  if(type.id()==ID_array)  {    // any arrays must have a size    const typet &result_type=follow(result.type());    assert(result_type.id()==ID_array &&           to_array_type(result_type).size().is_not_nil());    // we don't allow initialisation with symbols of array type    if(result.id()!=ID_array)    {      err_location(result);      error() << "invalid array initializer " << to_string(result)              << eom;      throw 0;    }  }  initializer=result;}

bool c_typecheck_baset::is_complete_type(const typet &type) const{  if(type.id()==ID_incomplete_struct ||     type.id()==ID_incomplete_union)    return false;  else if(type.id()==ID_array)  {    if(to_array_type(type).size().is_nil()) return false;    return is_complete_type(type.subtype());  }  else if(type.id()==ID_struct || type.id()==ID_union)  {    const struct_union_typet::componentst &components=      to_struct_union_type(type).components();    for(struct_union_typet::componentst::const_iterator        it=components.begin();        it!=components.end();        it++)      if(!is_complete_type(it->type()))        return false;  }  else if(type.id()==ID_vector)    return is_complete_type(type.subtype());  else if(type.id()==ID_symbol)    return is_complete_type(follow(type));  return true;}

smt_astt array_sym_smt_ast::eq(smt_convt *ctx, smt_astt other) const{  // We have two tuple_sym_smt_asts and need to create a boolean ast representing  // their equality: iterate over all their members, compute an equality for  // each of them, and then combine that into a final ast.  tuple_sym_smt_astt ta = this;  tuple_sym_smt_astt tb = to_tuple_sym_ast(other);  assert(is_array_type(sort->get_tuple_type()));  const array_type2t &arrtype = to_array_type(sort->get_tuple_type());  const struct_union_data &data = ctx->get_type_def(arrtype.subtype);  smt_convt::ast_vec eqs;  eqs.reserve(data.members.size());  // Iterate through each field and encode an equality.  unsigned int i = 0;  for(auto const &it : data.members)  {    type2tc tmparrtype(      new array_type2t(it, arrtype.array_size, arrtype.size_is_infinite));    smt_astt side1 = ta->project(ctx, i);    smt_astt side2 = tb->project(ctx, i);    eqs.push_back(side1->eq(ctx, side2));    i++;  }  // Create an ast representing the fact that all the members are equal.  return ctx->make_n_ary(ctx, &smt_convt::mk_and, eqs);}

void boolbvt::convert_with(  const typet &type,  const exprt &op1,  const exprt &op2,  const bvt &prev_bv,  bvt &next_bv){  // we only do that on arrays, bitvectors, structs, and unions  next_bv.resize(prev_bv.size());  if(type.id()==ID_array)    return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);  else if(type.id()==ID_bv ||          type.id()==ID_unsignedbv ||          type.id()==ID_signedbv)    return convert_with_bv(type, op1, op2, prev_bv, next_bv);  else if(type.id()==ID_struct)    return convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);  else if(type.id()==ID_union)    return convert_with_union(to_union_type(type), op1, op2, prev_bv, next_bv);  else if(type.id()==ID_symbol)    return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);  error().source_location=type.source_location();  error() << "unexpected with type: " << type.id();  throw 0;}

void boolbvt::convert_index(  const exprt &array,  const mp_integer &index,  bvt &bv){  const array_typet &array_type=    to_array_type(ns.follow(array.type()));  unsigned width=boolbv_width(array_type.subtype());  if(width==0)    return conversion_failed(array, bv);  bv.resize(width);    const bvt &tmp=convert_bv(array); // recursive call  mp_integer offset=index*width;  if(offset>=0 &&     offset+width<=mp_integer(tmp.size()))  {    // in bounds    for(unsigned i=0; i<width; i++)      bv[i]=tmp[integer2long(offset+i)];  }  else  {    // out of bounds    for(unsigned i=0; i<width; i++)      bv[i]=prop.new_variable();  }}

void base_type_rec(  typet &type, const namespacet &ns, std::set<irep_idt> &symb){  if(type.id()==ID_symbol ||     type.id()==ID_c_enum_tag ||     type.id()==ID_struct_tag ||     type.id()==ID_union_tag)  {    const symbolt *symbol;    if(!ns.lookup(type.get(ID_identifier), symbol) &&       symbol->is_type &&       !symbol->type.is_nil())    {      type=symbol->type;      base_type_rec(type, ns, symb); // recursive call      return;    }  }  else if(type.id()==ID_array)  {    base_type_rec(to_array_type(type).subtype(), ns, symb);  }  else if(type.id()==ID_struct ||          type.id()==ID_union)  {    struct_union_typet::componentst &components=      to_struct_union_type(type).components();    for(auto &component : components)      base_type_rec(component.type(), ns, symb);  }  else if(type.id()==ID_pointer)  {    typet &subtype=to_pointer_type(type).subtype();    // we need to avoid running into an infinite loop    if(subtype.id()==ID_symbol ||       subtype.id()==ID_c_enum_tag ||       subtype.id()==ID_struct_tag ||       subtype.id()==ID_union_tag)    {      const irep_idt &id=subtype.get(ID_identifier);      if(symb.find(id)!=symb.end())        return;      symb.insert(id);      base_type_rec(subtype, ns, symb);      symb.erase(id);    }    else      base_type_rec(subtype, ns, symb);  }}

void c_typecheck_baset::do_initializer(symbolt &symbol){  // this one doesn't need initialization  if(has_prefix(id2string(symbol.name), CPROVER_PREFIX "constant_infinity"))    return;  if(symbol.is_static_lifetime)  {    if(symbol.value.is_not_nil())    {      typecheck_expr(symbol.value);      do_initializer(symbol.value, symbol.type, true);      // need to adjust size?      if(follow(symbol.type).id()==ID_array &&         to_array_type(follow(symbol.type)).size().is_nil())        symbol.type=symbol.value.type();    }  }  else if(!symbol.is_type)  {    if(symbol.is_macro)    {      // these must have a constant value      assert(symbol.value.is_not_nil());      typecheck_expr(symbol.value);      source_locationt location=symbol.value.source_location();      do_initializer(symbol.value, symbol.type, true);      make_constant(symbol.value);    }    else if(symbol.value.is_not_nil())    {      typecheck_expr(symbol.value);      do_initializer(symbol.value, symbol.type, true);      // need to adjust size?      if(follow(symbol.type).id()==ID_array &&         to_array_type(follow(symbol.type)).size().is_nil())        symbol.type=symbol.value.type();    }  }}

void cpp_typecheckt::check_fixed_size_array(typet &type){  if(type.id()==ID_array)  {    array_typet &array_type=to_array_type(type);        if(array_type.size().is_not_nil())      make_constant_index(array_type.size());    // recursive call for multi-dimensional arrays    check_fixed_size_array(array_type.subtype());  }}

exprt path_symex_statet::array_theory(const exprt &src, bool propagate){  // top-level constant-sized arrays only right now  if(src.id()==ID_index)  {    const index_exprt &index_expr=to_index_expr(src);    exprt index_tmp1=read(index_expr.index(), propagate);    exprt index_tmp2=simplify_expr(index_tmp1, var_map.ns);    if(!index_tmp2.is_constant())    {      const array_typet &array_type=to_array_type(index_expr.array().type());      const typet &subtype=array_type.subtype();      if(array_type.size().is_constant())      {        mp_integer size;        if(to_integer(array_type.size(), size))          throw "failed to convert array size";        std::size_t size_int=integer2size_t(size);        exprt result=nil_exprt();        // split it up        for(std::size_t i=0; i<size_int; ++i)        {          exprt index=from_integer(i, index_expr.index().type());          exprt new_src=index_exprt(index_expr.array(), index, subtype);          if(result.is_nil())            result=new_src;          else          {            equal_exprt index_equal(index_expr.index(), index);            result=if_exprt(index_equal, new_src, result);          }        }        return result; // done      }      else      {        // TODO: variable-sized array      }    }  }  return src;}

exprt boolbvt::get(const exprt &expr) const{  if(expr.id()==ID_symbol ||     expr.id()==ID_nondet_symbol)  {    const irep_idt &identifier=expr.get(ID_identifier);        boolbv_mapt::mappingt::const_iterator it=      map.mapping.find(identifier);    if(it!=map.mapping.end())    {      const boolbv_mapt::map_entryt &map_entry=it->second;          if(is_unbounded_array(map_entry.type))        return bv_get_unbounded_array(identifier, to_array_type(map_entry.type));              std::vector<bool> unknown;      bvt bv;      unsigned width=map_entry.width;      bv.resize(width);      unknown.resize(width);      for(unsigned bit_nr=0; bit_nr<width; bit_nr++)      {        assert(bit_nr<map_entry.literal_map.size());        if(map_entry.literal_map[bit_nr].is_set)        {          unknown[bit_nr]=false;          bv[bit_nr]=map_entry.literal_map[bit_nr].l;        }        else        {          unknown[bit_nr]=true;          bv[bit_nr].clear();        }      }      return bv_get_rec(bv, unknown, 0, map_entry.type);    }  }  else if(expr.id()==ID_constant)    return expr;  else if(expr.id()==ID_infinity)    return expr;  return SUB::get(expr);}

void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol){  if(symbol.is_parameter)    adjust_function_parameter(symbol.type);  // check initializer, if needed  if(symbol.type.id()==ID_code)  {    if(symbol.value.is_not_nil())      typecheck_function_body(symbol);    else    {      // we don't need the identifiers      code_typet &code_type=to_code_type(symbol.type);      for(code_typet::parameterst::iterator          it=code_type.parameters().begin();          it!=code_type.parameters().end();          it++)        it->set_identifier(irep_idt());    }  }  else  {    if(symbol.type.id()==ID_array &&       to_array_type(symbol.type).size().is_nil() &&       !symbol.is_type)    {      // Insert a new type symbol for the array.      // We do this because we want a convenient way      // of adjusting the size of the type later on.      type_symbolt new_symbol(symbol.type);      new_symbol.name=id2string(symbol.name)+"$type";      new_symbol.base_name=id2string(symbol.base_name)+"$type";       new_symbol.location=symbol.location;      new_symbol.mode=symbol.mode;      new_symbol.module=symbol.module;          symbol.type=symbol_typet(new_symbol.name);          symbolt *new_sp;      symbol_table.move(new_symbol, new_sp);    }    // check the initializer    do_initializer(symbol);  }}

bvt boolbvt::convert_array_of(const array_of_exprt &expr){  if(expr.type().id()!=ID_array)    throw "array_of must be array-typed";  const array_typet &array_type=to_array_type(expr.type());  if(is_unbounded_array(array_type))    return conversion_failed(expr);  std::size_t width=boolbv_width(array_type);  if(width==0)  {    // A zero-length array is acceptable;    // an element with unknown size is not.    if(boolbv_width(array_type.subtype())==0)      return conversion_failed(expr);    else      return bvt();  }  const exprt &array_size=array_type.size();  mp_integer size;  if(to_integer(array_size, size))    return conversion_failed(expr);  const bvt &tmp=convert_bv(expr.op0());  bvt bv;  bv.resize(width);  if(size*tmp.size()!=width)    throw "convert_array_of: unexpected operand width";  std::size_t offset=0;  for(mp_integer i=0; i<size; i=i+1)  {    for(std::size_t j=0; j<tmp.size(); j++, offset++)      bv[offset]=tmp[j];  }  assert(offset==bv.size());  return bv;}

void array_sym_smt_ast::assign(smt_convt *ctx, smt_astt sym) const{  // We have two tuple_sym_smt_asts and need to call assign on all of their  // components.  array_sym_smt_astt src = this;  array_sym_smt_astt dst = to_array_sym_ast(sym);  const array_type2t &arrtype = to_array_type(sort->get_tuple_type());  const struct_union_data &data = ctx->get_type_def(arrtype.subtype);  unsigned int i = 0;  for(auto const &it : data.members)  {    array_type2tc tmparrtype(it, arrtype.array_size, arrtype.size_is_infinite);    smt_astt source = src->project(ctx, i);    smt_astt destination = dst->project(ctx, i);    source->assign(ctx, destination);    i++;  }}

void java_bytecode_typecheckt::typecheck_type(typet &type){  if(type.id()==ID_symbol)  {    irep_idt identifier=to_symbol_type(type).get_identifier();    symbol_tablet::symbolst::const_iterator s_it=      symbol_table.symbols.find(identifier);    // must exist already in the symbol table    if(s_it==symbol_table.symbols.end())    {      error() << "failed to find type symbol "<< identifier << eom;      throw 0;    }    assert(s_it->second.is_type);  }  else if(type.id()==ID_pointer)  {    typecheck_type(type.subtype());  }  else if(type.id()==ID_array)  {    typecheck_type(type.subtype());    typecheck_expr(to_array_type(type).size());  }  else if(type.id()==ID_code)  {    code_typet &code_type=to_code_type(type);    typecheck_type(code_type.return_type());    code_typet::parameterst &parameters=code_type.parameters();    for(code_typet::parameterst::iterator        it=parameters.begin(); it!=parameters.end(); it++)      typecheck_type(it->type());  }}

bool goto_symex_statet::constant_propagation(const expr2tc &expr) const{  static unsigned int with_counter=0;  // Don't permit const propagaion of infinite-size arrays. They're going to  // be special modelling arrays that require special handling either at SMT  // or some other level, so attempting to optimse them is a Bad Plan (TM).  if (is_array_type(expr) && to_array_type(expr->type).size_is_infinite)    return false;  if (is_nil_expr(expr)) {    return true; // It's fine to constant propagate something that's absent.  } else if (is_constant_expr(expr)) {    return true;  }  else if (is_symbol2t(expr) && to_symbol2t(expr).thename == "NULL")  {    // Null is also essentially a constant.    return true;  }  else if (is_address_of2t(expr))  {    return constant_propagation_reference(to_address_of2t(expr).ptr_obj);  }  else if (is_typecast2t(expr))  {    return constant_propagation(to_typecast2t(expr).from);  }  else if (is_add2t(expr))  {    forall_operands2(it, idx, expr)      if(!constant_propagation(*it))        return false;    return true;  }  else if (is_constant_array_of2t(expr))

exprt flatten_byte_extract(  const exprt &src,  const namespacet &ns){  assert(src.id()==ID_byte_extract_little_endian ||         src.id()==ID_byte_extract_big_endian);  assert(src.operands().size()==2);  bool little_endian;    if(src.id()==ID_byte_extract_little_endian)    little_endian=true;  else if(src.id()==ID_byte_extract_big_endian)    little_endian=false;  else    assert(false);    if(src.id()==ID_byte_extract_big_endian)     throw "byte_extract flattening of big endian not done yet";  unsigned width=    integer2long(pointer_offset_size(ns, src.type()));    const typet &t=src.op0().type();    if(t.id()==ID_array)  {    const array_typet &array_type=to_array_type(t);    const typet &subtype=array_type.subtype();        // byte-array?    if((subtype.id()==ID_unsignedbv ||        subtype.id()==ID_signedbv) &&       subtype.get_int(ID_width)==8)    {      // get 'width'-many bytes, and concatenate      exprt::operandst op;      op.resize(width);            for(unsigned i=0; i<width; i++)      {        // the most significant byte comes first in the concatenation!        unsigned offset_i=          little_endian?(width-i-1):i;                plus_exprt offset(from_integer(offset_i, src.op1().type()), src.op1());        index_exprt index_expr(subtype);        index_expr.array()=src.op0();        index_expr.index()=offset;        op[i]=index_expr;      }            if(width==1)        return op[0];      else // width>=2      {        concatenation_exprt concatenation(src.type());        concatenation.operands().swap(op);        return concatenation;      }    }    else // non-byte array    {      const exprt &root=src.op0();      const exprt &offset=src.op1();      const typet &array_type=ns.follow(root.type());      const typet &offset_type=ns.follow(offset.type());      const typet &element_type=ns.follow(array_type.subtype());      mp_integer element_width=pointer_offset_size(ns, element_type);            if(element_width==-1) // failed        throw "failed to flatten non-byte array with unknown element width";      mp_integer result_width=pointer_offset_size(ns, src.type());      mp_integer num_elements=(element_width+result_width-2)/element_width+1;      // compute new root and offset      concatenation_exprt concat(        unsignedbv_typet(integer2long(element_width*8*num_elements)));      exprt first_index=        (element_width==1)?offset         : div_exprt(offset, from_integer(element_width, offset_type)); // 8*offset/el_w      for(mp_integer i=num_elements; i>0; --i)      {        plus_exprt index(first_index, from_integer(i-1, offset_type));        concat.copy_to_operands(index_exprt(root, index));      }      // the new offset is width%offset      exprt new_offset=        (element_width==1)?from_integer(0, offset_type):        mod_exprt(offset, from_integer(element_width, offset_type));      // build new byte-extract expression      exprt tmp(src.id(), src.type());      tmp.copy_to_operands(concat, new_offset);      return tmp;//.........这里部分代码省略.........

exprt flatten_byte_update(  const exprt &src,  const namespacet &ns){  assert(src.id()==ID_byte_update_little_endian ||         src.id()==ID_byte_update_big_endian);  assert(src.operands().size()==3);  mp_integer element_size=    pointer_offset_size(ns, src.op2().type());    const typet &t=ns.follow(src.op0().type());    if(t.id()==ID_array)  {    const array_typet &array_type=to_array_type(t);    const typet &subtype=array_type.subtype();        // array of bitvectors?    if(subtype.id()==ID_unsignedbv ||       subtype.id()==ID_signedbv ||       subtype.id()==ID_floatbv)    {      mp_integer sub_size=pointer_offset_size(ns, subtype);            if(sub_size==-1)        throw "can't flatten byte_update for sub-type without size";      // byte array?      if(sub_size==1)      {        // apply 'array-update-with' element_size times        exprt result=src.op0();                for(mp_integer i=0; i<element_size; ++i)        {          exprt i_expr=from_integer(i, ns.follow(src.op1().type()));          exprt new_value;                    if(i==0 && element_size==1) // bytes?          {            new_value=src.op2();            if(new_value.type()!=subtype)              new_value.make_typecast(subtype);          }          else          {            exprt byte_extract_expr(              src.id()==ID_byte_update_little_endian?ID_byte_extract_little_endian:              src.id()==ID_byte_update_big_endian?ID_byte_extract_big_endian:              throw "unexpected src.id()",              subtype);                        byte_extract_expr.copy_to_operands(src.op2(), i_expr);            new_value=flatten_byte_extract(byte_extract_expr, ns);          }          exprt where=plus_exprt(src.op1(), i_expr);                      with_exprt with_expr;          with_expr.type()=src.type();          with_expr.old()=result;          with_expr.where()=where;          with_expr.new_value()=new_value;                    result.swap(with_expr);        }                return result;      }      else // sub_size!=1      {        if(element_size==1) // byte-granularity update        {          div_exprt div_offset(src.op1(), from_integer(sub_size, src.op1().type()));          mod_exprt mod_offset(src.op1(), from_integer(sub_size, src.op1().type()));                  index_exprt index_expr(src.op0(), div_offset, array_type.subtype());                    exprt byte_update_expr(src.id(), array_type.subtype());          byte_update_expr.copy_to_operands(index_expr, mod_offset, src.op2());          // Call recurisvely, the array is gone!                      exprt flattened_byte_update_expr=            flatten_byte_update(byte_update_expr, ns);                      with_exprt with_expr(            src.op0(), div_offset, flattened_byte_update_expr);                      return with_expr;        }        else          throw "flatten_byte_update can only do byte updates of non-byte arrays right now";      }    }    else    {      throw "flatten_byte_update can only do arrays of scalars right now";    }//.........这里部分代码省略.........

//.........这里部分代码省略.........    {      // count the bits      bit_field_bits+=it->type().get_int(ID_width);          // we consider the type for max_alignment, however      unsigned a=alignment(it->get_bit_field_type(), ns);      if(max_alignment<a)         max_alignment=a;      continue;    }    else if(bit_field_bits!=0)    {      // these are now assumed to be multiples of 8      offset+=bit_field_bits/8;      bit_field_bits=0;    }        const typet &it_type=it->type();    unsigned a=alignment(it_type, ns);        // check minimum alignment    if(a<config.ansi_c.alignment)      a=config.ansi_c.alignment;          if(max_alignment<a)       max_alignment=a;      if(a!=1)    {      // we may need to align it      unsigned displacement=integer2long(offset%a);      if(displacement!=0)      {        unsigned pad=a-displacement;              unsignedbv_typet padding_type;        padding_type.set_width(pad*8);                struct_typet::componentt component;        component.type()=padding_type;        component.set_name("$pad"+i2string(padding_counter++));        component.set_is_padding(true);                it=components.insert(it, component);        it++; // skip over                offset+=pad;      }    }        mp_integer size=pointer_offset_size(ns, it_type);        if(size!=-1)      offset+=size;  }    if(bit_field_bits!=0)  {    // these are now assumed to be multiples of 8    offset+=bit_field_bits/8;  }  // There may be a need for 'end of struct' padding.  // We use 'max_alignment'.  if(max_alignment>1)  {    // we may need to align it    unsigned displacement=integer2long(offset%max_alignment);    if(displacement!=0)    {      unsigned pad=max_alignment-displacement;          unsignedbv_typet padding_type;      padding_type.set_width(pad*8);      struct_typet::componentst::iterator it;            // we need to insert before any 'flexible member'      if(!components.empty() &&         components.back().type().id()==ID_array &&         to_array_type(components.back().type()).size().is_zero())      {        it=components.end();        it--;      }      else        it=components.end();      struct_typet::componentt component;      component.type()=padding_type;      component.set_name("$pad"+i2string(padding_counter++));      component.set_is_padding(true);            components.insert(it, component);    }  }}

bool static_lifetime_init(  symbol_tablet &symbol_table,  const source_locationt &source_location,  message_handlert &message_handler){  namespacet ns(symbol_table);  symbol_tablet::symbolst::iterator s_it=    symbol_table.symbols.find(INITIALIZE_FUNCTION);  if(s_it==symbol_table.symbols.end())    return false;  symbolt &init_symbol=s_it->second;  init_symbol.value=code_blockt();  init_symbol.value.add_source_location()=source_location;  code_blockt &dest=to_code_block(to_code(init_symbol.value));  // add the magic label to hide  dest.add(code_labelt("__CPROVER_HIDE", code_skipt()));  // do assignments based on "value"  // sort alphabetically for reproducible results  std::set<std::string> symbols;  forall_symbols(it, symbol_table.symbols)    symbols.insert(id2string(it->first));  for(const std::string &id : symbols)  {    const symbolt &symbol=ns.lookup(id);    const irep_idt &identifier=symbol.name;    if(!symbol.is_static_lifetime)      continue;    if(symbol.is_type || symbol.is_macro)      continue;    // special values    if(identifier==CPROVER_PREFIX "constant_infinity_uint" ||       identifier==CPROVER_PREFIX "memory" ||       identifier=="__func__" ||       identifier=="__FUNCTION__" ||       identifier=="__PRETTY_FUNCTION__" ||       identifier=="argc'" ||       identifier=="argv'" ||       identifier=="envp'" ||       identifier=="envp_size'")      continue;    // just for linking    if(has_prefix(id, CPROVER_PREFIX "architecture_"))      continue;    const typet &type=ns.follow(symbol.type);    // check type    if(type.id()==ID_code ||       type.id()==ID_empty)      continue;    // We won't try to initialize any symbols that have    // remained incomplete.    if(symbol.value.is_nil() &&       symbol.is_extern)      // Compilers would usually complain about these      // symbols being undefined.      continue;    if(type.id()==ID_array &&       to_array_type(type).size().is_nil())    {      // C standard 6.9.2, paragraph 5      // adjust the type to an array of size 1      symbol_tablet::symbolst::iterator it=        symbol_table.symbols.find(identifier);      assert(it!=symbol_table.symbols.end());      it->second.type=type;      it->second.type.set(ID_size, from_integer(1, size_type()));    }    if(type.id()==ID_incomplete_struct ||       type.id()==ID_incomplete_union)      continue; // do not initialize    if(symbol.value.id()==ID_nondet)      continue; // do not initialize    exprt rhs;    if(symbol.value.is_nil())    {      try//.........这里部分代码省略.........

const typet &control_array_size_type(const symbol_tablet &st){  const struct_typet::componentt &c=get_comp(st, CEGIS_CONTROL_A_MEMBER_NAME);  return to_array_type(c.type()).size().type();}