diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 8c2c9d62628..4b3a4a0f339 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -216,13 +216,20 @@ void ansi_c_convert_typet::read_rec(const typet &type) { c_storage_spec.alias=type.subtype().get(ID_value); } - else if(type.id()==ID_pointer) + else if(type.id()==ID_frontend_pointer) { - // pointers have a width, much like integers - pointer_typet tmp=to_pointer_type(type); - tmp.set_width(config.ansi_c.pointer_width); + // We turn ID_frontend_pointer to ID_pointer + // Pointers have a width, much like integers, + // which is added here. + typet tmp(type); + tmp.id(ID_pointer); + tmp.set(ID_width, config.ansi_c.pointer_width); other.push_back(tmp); } + else if(type.id()==ID_pointer) + { + UNREACHABLE; + } else other.push_back(type); } diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index a0ef86cffe0..74f05e926b5 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -98,7 +98,7 @@ typet ansi_c_declarationt::full_type( // this gets types that are still raw parse trees while(p->is_not_nil()) { - if(p->id()==ID_pointer || p->id()==ID_array || + if(p->id()==ID_frontend_pointer || p->id()==ID_array || p->id()==ID_vector || p->id()==ID_c_bit_field || p->id()==ID_block_pointer || p->id()==ID_code) p=&p->subtype(); diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 88ca770c4bf..a047108d1b0 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -1492,19 +1492,22 @@ void c_typecheck_baset::adjust_function_parameter(typet &type) const { if(type.id()==ID_array) { + source_locationt source_location=type.source_location(); type=pointer_type(type.subtype()); - type.remove(ID_size); - type.remove(ID_C_constant); + type.add_source_location()=source_location; } else if(type.id()==ID_code) { // see ISO/IEC 9899:1999 page 199 clause 8, // may be hidden in typedef + source_locationt source_location=type.source_location(); type=pointer_type(type); + type.add_source_location()=source_location; } else if(type.id()==ID_KnR) { // any KnR args without type yet? type=signed_int_type(); // the default is integer! + // no source location } } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index ba7ab7a0bb1..ce04136d8e2 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -3065,7 +3065,10 @@ unary_identifier_declarator: { // the type_qualifier_list is for the pointer, // and not the identifier_declarator - stack_type($1)=pointer_type(typet(ID_abstract)); + // The below is deliberately not using pointer_type(); + // the width is added during conversion. + stack_type($1).id(ID_frontend_pointer); + stack_type($1).subtype()=typet(ID_abstract); $2=merge($2, $1); // dest=$2 make_subtype($3, $2); // dest=$3 $$=$3; @@ -3249,13 +3252,19 @@ unary_abstract_declarator: '*' { $$=$1; - stack_type($$)=pointer_type(typet(ID_abstract)); + // The below is deliberately not using pointer_type(); + // the width is added during conversion. + stack_type($$).id(ID_frontend_pointer); + stack_type($$).subtype()=typet(ID_abstract); } | '*' attribute_type_qualifier_list { // The type_qualifier_list belongs to the pointer, // not to the (missing) abstract declarator. - stack_type($1)=pointer_type(typet(ID_abstract)); + // The below is deliberately not using pointer_type(); + // the width is added during conversion. + stack_type($1).id(ID_frontend_pointer); + stack_type($1).subtype()=typet(ID_abstract); $$=merge($2, $1); } | '*' abstract_declarator @@ -3267,7 +3276,10 @@ unary_abstract_declarator: { // The type_qualifier_list belongs to the pointer, // not to the abstract declarator. - stack_type($1)=pointer_type(typet(ID_abstract)); + // The below is deliberately not using pointer_type(); + // the width is added during conversion. + stack_type($1).id(ID_frontend_pointer); + stack_type($1).subtype()=typet(ID_abstract); $2=merge($2, $1); // dest=$2 make_subtype($3, $2); // dest=$3 $$=$3; @@ -3286,13 +3298,19 @@ parameter_unary_abstract_declarator: '*' { $$=$1; - stack_type($$)=pointer_type(typet(ID_abstract)); + // The below is deliberately not using pointer_type(); + // the width is added during conversion. + stack_type($$).id(ID_frontend_pointer); + stack_type($$).subtype()=typet(ID_abstract); } | '*' attribute_type_qualifier_list { // The type_qualifier_list belongs to the pointer, // not to the (missing) abstract declarator. - stack_type($1)=pointer_type(typet(ID_abstract)); + // The below is deliberately not using pointer_type(); + // the width is added during conversion. + stack_type($1).id(ID_frontend_pointer); + stack_type($1).subtype()=typet(ID_abstract); $$=merge($2, $1); } | '*' parameter_abstract_declarator @@ -3304,7 +3322,10 @@ parameter_unary_abstract_declarator: { // The type_qualifier_list belongs to the pointer, // not to the (missing) abstract declarator. - stack_type($1)=pointer_type(typet(ID_abstract)); + // The below is deliberately not using pointer_type(); + // the width is added during conversion. + stack_type($1).id(ID_frontend_pointer); + stack_type($1).subtype()=typet(ID_abstract); $2=merge($2, $1); // dest=$2 make_subtype($3, $2); // dest=$3 $$=$3; diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc index 6f0b3f41b1d..68f9d759ca5 100644 --- a/src/ansi-c/parser_static.inc +++ b/src/ansi-c/parser_static.inc @@ -187,7 +187,7 @@ static void make_subtype(typet &dest, typet &src) #endif assert(src.id()==ID_array || - src.id()==ID_pointer || + src.id()==ID_frontend_pointer || src.id()==ID_code || src.id()==ID_merged_type || src.id()==ID_abstract || @@ -207,7 +207,7 @@ static void make_subtype(typet &dest, typet &src) sub=&(p->subtypes().back()); } - if(sub->id()==ID_pointer || + if(sub->id()==ID_frontend_pointer || sub->id()==ID_array || sub->id()==ID_code) { @@ -290,7 +290,10 @@ Function: make_pointer static void make_pointer(const YYSTYPE dest) { - stack_type(dest)=pointer_type(typet(ID_abstract)); + // The below deliberately avoids pointer_type(). + // The width is set during conversion. + stack_type(dest).id(ID_frontend_pointer); + stack_type(dest).subtype()=typet(ID_abstract); } /*******************************************************************\ diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index ae5853d07b3..23d4ae5acbd 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -159,6 +159,19 @@ void cpp_convert_typet::read_rec(const typet &type) tmp.id(ID_empty); other.push_back(tmp); } + else if(type.id()==ID_frontend_pointer) + { + // add width and turn into ID_pointer + typet tmp=type; + tmp.id(ID_pointer); + tmp.set(ID_width, config.ansi_c.pointer_width); + other.push_back(tmp); + } + else if(type.id()==ID_pointer) + { + // ignore, we unfortunately convert multiple times + other.push_back(type); + } else { other.push_back(type); @@ -549,7 +562,6 @@ void cpp_convert_plain_type(typet &type) if(type.id()==ID_cpp_name || type.id()==ID_struct || type.id()==ID_union || - type.id()==ID_pointer || type.id()==ID_array || type.id()==ID_code || type.id()==ID_unsignedbv || diff --git a/src/cpp/cpp_convert_type.h b/src/cpp/cpp_convert_type.h index 590ce6e98a6..0a14982210b 100644 --- a/src/cpp/cpp_convert_type.h +++ b/src/cpp/cpp_convert_type.h @@ -14,6 +14,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -void cpp_convert_plain_type(typet &type); +void cpp_convert_plain_type(typet &); #endif // CPROVER_CPP_CPP_CONVERT_TYPE_H diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 4de000d02eb..60dc1a50920 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -18,9 +18,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include -#include #include +#include #include "cpp_token_buffer.h" #include "cpp_member_spec.h" @@ -3016,7 +3016,7 @@ bool Parser::optPtrOperator(typet &ptrs) if(t=='*') { - typet op=pointer_type(typet(ID_nil)); + typet op(ID_frontend_pointer); // width gets set during conversion cpp_tokent tk; lex.get_token(tk); set_location(op, tk); @@ -3079,7 +3079,7 @@ bool Parser::optPtrOperator(typet &ptrs) { cpp_tokent tk; lex.get_token(tk); - typet op=pointer_type(typet(ID_nil)); + typet op(ID_frontend_pointer); // width gets set during conversion op.set(ID_C_reference, true); set_location(op, tk); t_list.push_front(op); @@ -3088,7 +3088,7 @@ bool Parser::optPtrOperator(typet &ptrs) { cpp_tokent tk; lex.get_token(tk); - typet op=pointer_type(typet(ID_nil)); + typet op(ID_frontend_pointer); // width gets set during conversion op.set(ID_C_rvalue_reference, true); set_location(op, tk); t_list.push_front(op); @@ -3531,7 +3531,7 @@ bool Parser::rPtrToMember(irept &ptr_to_mem) std::cout << std::string(__indent, ' ') << "Parser::rPtrToMember 0\n"; #endif - typet ptm=pointer_type(typet(ID_nil)); + typet ptm(ID_frontend_pointer); // width gets set during conversion irept &name = ptm.add("to-member"); name=cpp_namet(); irept::subt &components=name.get_sub(); @@ -6478,6 +6478,7 @@ bool Parser::rPrimaryExpr(exprt &exp) case TOK_NULLPTR: lex.get_token(tk); + // as an exception, we set the width of pointer exp=constant_exprt(ID_NULL, pointer_type(typet(ID_nullptr))); set_location(exp, tk); #ifdef DEBUG diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index cb8e1c89dd3..fca18c8693b 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -104,6 +104,7 @@ IREP_ID_ONE(skip) IREP_ID_ONE(arguments) IREP_ID_ONE(array) IREP_ID_ONE(size) +IREP_ID_ONE(frontend_pointer) IREP_ID_ONE(pointer) IREP_ID_ONE(block_pointer) IREP_ID_ONE(switch)