Ensure pointer invariants are maintained

CMakeLists.txt

@@ -3,6 +3,7 @@ cmake_minimum_required(VERSION 3.2)
 find_program(CCACHE_PROGRAM ccache)
 if(CCACHE_PROGRAM)
     set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
+    message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
  endif()
 
 set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
@@ -19,7 +20,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     #   Ensure NDEBUG is not set for release builds
     set(CMAKE_CXX_FLAGS_RELEASE "-O2")
     #   Enable lots of warnings
-    set(CMAKE_CXX_FLAGS "-Wall -Wpedantic -Werror")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     #   This would be the place to enable warnings for Windows builds, although
     #   config.inc doesn't seem to do that currently

regression/ansi-c/arch_flags_mcpu_good/test.desc

@@ -14,6 +14,10 @@ command line:
 
   goto-cc --native-compiler=arm-none-eabi-gcc -mcpu=cortex-a15 -c source.c
 
+On Ubuntu, you can get a suitable compiler using:
+
+  sudo apt install gcc-arm-none-eabi
+
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
 local machine. Linking it together with the ARM object file, while

regression/ansi-c/arch_flags_mthumb_good/test.desc

@@ -14,6 +14,10 @@ line:
 
   goto-cc --native-compiler=arm-none-eabi-gcc -mthumb -c source.c
 
+On Ubuntu, you can get a suitable compiler using:
+
+  sudo apt install gcc-arm-none-eabi
+
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
 local machine. Linking it together with the ARM object file, while

src/CMakeLists.txt

@@ -165,7 +165,6 @@ add_subdirectory(util)
 add_subdirectory(xmllang)
 add_subdirectory(java_bytecode)
 add_subdirectory(miniz)
-add_subdirectory(musketeer)
 add_subdirectory(clobber)
 add_subdirectory(cbmc)
 add_subdirectory(goto-cc)

src/ansi-c/c_typecast.cpp

@@ -372,8 +372,7 @@ void c_typecastt::implicit_typecast_arithmetic(
   case PTR:
     if(expr_type.id()==ID_array)
     {
-      new_type.id(ID_pointer);
-      new_type.subtype()=expr_type.subtype();
+      new_type=pointer_type(expr_type.subtype());
       break;
     }
     return;

src/ansi-c/c_typecheck_expr.cpp

@@ -1594,8 +1594,7 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
     {
       // Make it void *.
       // gcc and clang issue a warning for this.
-      expr.type()=typet(ID_pointer);
-      expr.type().subtype()=typet(ID_empty);
+      expr.type()=pointer_type(empty_typet());
       implicit_typecast(operands[1], expr.type());
       implicit_typecast(operands[2], expr.type());
     }

src/ansi-c/c_typecheck_type.cpp

@@ -1492,7 +1492,7 @@ void c_typecheck_baset::adjust_function_parameter(typet &type) const
 {
   if(type.id()==ID_array)
   {
-    type.id(ID_pointer);
+    type=pointer_type(type.subtype());
     type.remove(ID_size);
     type.remove(ID_C_constant);
   }

src/ansi-c/parser.y

@@ -3065,8 +3065,7 @@ unary_identifier_declarator:
         {
           // the type_qualifier_list is for the pointer,
           // and not the identifier_declarator
-          stack_type($1).id(ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;
@@ -3250,15 +3249,13 @@ unary_abstract_declarator:
           '*'
         {
           $$=$1;
-          set($$, ID_pointer);
-          stack_type($$).subtype()=typet(ID_abstract);
+          stack_type($$)=pointer_type(typet(ID_abstract));
         }
         | '*' attribute_type_qualifier_list
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          set($1, ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $$=merge($2, $1);
         }
         | '*' abstract_declarator
@@ -3270,8 +3267,7 @@ unary_abstract_declarator:
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the abstract declarator.
-          stack_type($1).id(ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;
@@ -3290,15 +3286,13 @@ parameter_unary_abstract_declarator:
           '*'
         {
           $$=$1;
-          set($$, ID_pointer);
-          stack_type($$).subtype()=typet(ID_abstract);
+          stack_type($$)=pointer_type(typet(ID_abstract));
         }
         | '*' attribute_type_qualifier_list
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          set($1, ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $$=merge($2, $1);
         }
         | '*' parameter_abstract_declarator
@@ -3310,8 +3304,7 @@ parameter_unary_abstract_declarator:
         {
           // The type_qualifier_list belongs to the pointer,
           // not to the (missing) abstract declarator.
-          stack($1).id(ID_pointer);
-          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1)=pointer_type(typet(ID_abstract));
           $2=merge($2, $1); // dest=$2
           make_subtype($3, $2); // dest=$3
           $$=$3;

src/ansi-c/parser_static.inc

@@ -290,8 +290,7 @@ Function: make_pointer
 
 static void make_pointer(const YYSTYPE dest)
 {
-  set(dest, ID_pointer);
-  stack_type(dest).subtype()=typet(ID_abstract);
+  stack_type(dest)=pointer_type(typet(ID_abstract));
 }
 
 /*******************************************************************\

src/cpp/cpp_typecheck_constructor.cpp

@@ -41,17 +41,17 @@ static void copy_parent(
   exprt &op0=code.op0().op0();
 
   op0.operands().push_back(exprt("cpp-this"));
-  op0.type().id(ID_pointer);
-  op0.type().subtype()=cpp_namet(parent_base_name, source_location).as_type();
+  op0.type()=
+    pointer_type(cpp_namet(parent_base_name, source_location).as_type());
   op0.add_source_location()=source_location;
 
   code.operands().push_back(exprt("explicit-typecast"));
   exprt &op1=code.op1();
 
-  op1.type().id(ID_pointer);
+  op0.type()=
+    pointer_type(cpp_namet(parent_base_name, source_location).as_type());
   op1.type().set(ID_C_reference, true);
   op1.type().subtype().set(ID_C_constant, true);
-  op1.type().subtype()=cpp_namet(parent_base_name, source_location).as_type();
 
   op1.operands().push_back(exprt(ID_cpp_name));
   op1.op0().get_sub().push_back(irept(ID_name));
@@ -420,9 +420,8 @@ void cpp_typecheckt::default_assignop(
   args_decl_declor.name().get_sub().back().add(ID_identifier).id(arg_name);
   args_decl_declor.add_source_location()=source_location;
 
-  args_decl_declor.type().id(ID_pointer);
+  args_decl_declor.type()=pointer_type(typet(ID_nil));
   args_decl_declor.type().set(ID_C_reference, true);
-  args_decl_declor.type().subtype().make_nil();
   args_decl_declor.value().make_nil();
 }
 

src/cpp/parse.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/c_types.h>
 
 #include <ansi-c/ansi_c_y.tab.h>
 
@@ -3015,7 +3016,7 @@ bool Parser::optPtrOperator(typet &ptrs)
 
     if(t=='*')
     {
-      typet op(ID_pointer);
+      typet op=pointer_type(typet(ID_nil));
       cpp_tokent tk;
       lex.get_token(tk);
       set_location(op, tk);
@@ -3078,7 +3079,7 @@ bool Parser::optPtrOperator(typet &ptrs)
     {
       cpp_tokent tk;
       lex.get_token(tk);
-      typet op(ID_pointer);
+      typet op=pointer_type(typet(ID_nil));
       op.set(ID_C_reference, true);
       set_location(op, tk);
       t_list.push_front(op);
@@ -3087,7 +3088,7 @@ bool Parser::optPtrOperator(typet &ptrs)
     {
       cpp_tokent tk;
       lex.get_token(tk);
-      typet op(ID_pointer);
+      typet op=pointer_type(typet(ID_nil));
       op.set(ID_C_rvalue_reference, true);
       set_location(op, tk);
       t_list.push_front(op);
@@ -3530,7 +3531,7 @@ bool Parser::rPtrToMember(irept &ptr_to_mem)
   std::cout << std::string(__indent, ' ') << "Parser::rPtrToMember 0\n";
   #endif
 
-  irept ptm(ID_pointer);
+  typet ptm=pointer_type(typet(ID_nil));
   irept &name = ptm.add("to-member");
   name=cpp_namet();
   irept::subt &components=name.get_sub();
@@ -6477,7 +6478,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
 
   case TOK_NULLPTR:
     lex.get_token(tk);
-    exp=constant_exprt(ID_NULL, typet(ID_pointer, typet(ID_nullptr)));
+    exp=constant_exprt(ID_NULL, pointer_type(typet(ID_nullptr)));
     set_location(exp, tk);
     #ifdef DEBUG
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 6\n";

src/goto-programs/remove_exceptions.cpp

@@ -213,7 +213,7 @@ void remove_exceptionst::add_exceptional_returns(
       new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
       new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
       new_symbol.mode=function_symbol.mode;
-      new_symbol.type=typet(ID_pointer, empty_typet());
+      new_symbol.type=pointer_type(empty_typet());
       symbol_table.add(new_symbol);
 
       // initialize the exceptional return with NULL