Merge pull request #1284 from diffblue/pointer-width-fixup

Pointer width fixup

Author: Daniel Kroening

src/goto-programs/builtin_functions.cpp

@@ -700,7 +700,7 @@ void goto_convertt::do_java_new_array(
   if(given_element_type.is_not_nil())
   {
     allocate_data_type=
-      pointer_typet(static_cast<const typet &>(given_element_type));
+      pointer_type(static_cast<const typet &>(given_element_type));
   }
   else
     allocate_data_type=data.type();

src/goto-programs/remove_exceptions.cpp

@@ -218,7 +218,7 @@ void remove_exceptionst::add_exceptional_returns(
 
       // initialize the exceptional return with NULL
       symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
-      null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
+      null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
       goto_programt::targett t_null=
         goto_program.insert_before(goto_program.instructions.begin());
       t_null->make_assignment();

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -311,12 +311,12 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
       id2string(symbol_type.get_identifier())+".clone:()Ljava/lang/Object;";
     code_typet clone_type;
     clone_type.return_type()=
-      pointer_typet(symbol_typet("java::java.lang.Object"));
+      java_reference_type(symbol_typet("java::java.lang.Object"));
     code_typet::parametert this_param;
     this_param.set_identifier(id2string(clone_name)+"::this");
     this_param.set_base_name("this");
     this_param.set_this();
-    this_param.type()=pointer_typet(symbol_type);
+    this_param.type()=java_reference_type(symbol_type);
     clone_type.parameters().push_back(this_param);
 
     parameter_symbolt this_symbol;
@@ -333,7 +333,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     local_symbol.name=local_name;
     local_symbol.base_name="cloned_array";
     local_symbol.pretty_name=local_symbol.base_name;
-    local_symbol.type=pointer_typet(symbol_type);
+    local_symbol.type=java_reference_type(symbol_type);
     local_symbol.mode=ID_java;
     symbol_table.add(local_symbol);
     const auto &local_symexpr=local_symbol.symbol_expr();
@@ -345,7 +345,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
     side_effect_exprt java_new_array(
       ID_java_new_array,
-      pointer_typet(symbol_type));
+      java_reference_type(symbol_type));
     dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
     dereference_exprt new_array(local_symexpr, symbol_type);
     member_exprt old_length(old_array, comp1.get_name(), comp1.type());

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1252,7 +1252,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       symbol_exprt catch_var=
         tmp_variable(
           "caught_exception",
-          pointer_typet(catch_type));
+          java_reference_type(catch_type));
       stack.push_back(catch_var);
       code_landingpadt catch_statement(catch_var);
       catch_instruction=catch_statement;
@@ -1673,7 +1673,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
         from_integer(
           std::next(i_it)->address,
           unsignedbv_typet(64));
-      results[0].type()=pointer_typet(void_typet(), 64);
+      results[0].type()=pointer_type(void_typet());
     }
     else if(statement=="ret")
     {
@@ -1698,7 +1698,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
             from_integer(
               jsr_ret_targets[idx],
               unsignedbv_typet(64));
-          address_ptr.type()=pointer_typet(void_typet(), 64);
+          address_ptr.type()=pointer_type(void_typet());
           branch.cond()=equal_exprt(retvar, address_ptr);
           branch.cond().add_source_location()=i_it->source_location;
           branch.then_case()=g;

src/java_bytecode/java_bytecode_instrument.cpp

@@ -13,6 +13,7 @@ Date:   June 2017
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
+#include <util/c_types.h>
 
 #include <goto-programs/goto_functions.h>
 
@@ -221,8 +222,7 @@ codet java_bytecode_instrumentt::check_class_cast(
   binary_predicate_exprt class_cast_check(
     class1, ID_java_instanceof, class2);
 
-  empty_typet voidt;
-  pointer_typet voidptr(voidt);
+  pointer_typet voidptr=pointer_type(empty_typet());
   exprt null_check_op=class1;
   if(null_check_op.type()!=voidptr)
     null_check_op.make_typecast(voidptr);

src/java_bytecode/java_string_library_preprocess.cpp

@@ -22,6 +22,8 @@ Date:   April 2017
 #include <util/fresh_symbol.h>
 #include <util/refined_string_type.h>
 #include <util/string_expr.h>
+#include <util/c_types.h>
+
 #include "java_types.h"
 #include "java_object_factory.h"
 #include "java_utils.h"
@@ -1168,7 +1170,7 @@ codet java_string_library_preprocesst::make_string_to_char_array_code(
 
   // data = new char[]
   exprt data=allocate_fresh_array(
-    pointer_typet(string_expr.content().type()), loc, symbol_table, code);
+    java_reference_type(string_expr.content().type()), loc, symbol_table, code);
 
   // *data = string_expr.content
   dereference_exprt deref_data(data, data.type().subtype());
@@ -1280,7 +1282,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
       struct_type.get_component("value");
     if(!value_comp.is_nil())
     {
-      pointer_typet pointer_type(struct_type);
+      pointer_typet pointer_type=::pointer_type(struct_type);
       dereference_exprt deref(
         typecast_exprt(object, pointer_type), pointer_type.subtype());
       member_exprt deref_value(deref, value_comp.get_name(), value_comp.type());
@@ -1308,7 +1310,7 @@ exprt java_string_library_preprocesst::get_object_at_index(
   int index)
 {
   dereference_exprt deref_objs(argv, argv.type().subtype());
-  pointer_typet empty_pointer((empty_typet()));
+  pointer_typet empty_pointer=pointer_type(empty_typet());
   pointer_typet pointer_of_pointer;
   pointer_of_pointer.copy_to_subtypes(empty_pointer);
   member_exprt data_member(deref_objs, "data", pointer_of_pointer);
@@ -1409,7 +1411,8 @@ exprt java_string_library_preprocesst::make_argument_for_format(
 
     if(name=="string_expr")
     {
-      pointer_typet string_pointer(symbol_typet("java::java.lang.String"));
+      pointer_typet string_pointer=
+        java_reference_type(symbol_typet("java::java.lang.String"));
       typecast_exprt arg_i_as_string(arg_i, string_pointer);
       code_not_null.add(code_assign_java_string_to_string_expr(
         to_string_expr(field_expr), arg_i_as_string, symbol_table));
@@ -1515,7 +1518,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
   code_blockt code;
 
   // > Class class1;
-  pointer_typet class_type(symbol_table.lookup("java::java.lang.Class").type);
+  pointer_typet class_type=
+    java_reference_type(symbol_table.lookup("java::java.lang.Class").type);
   symbolt class1_sym=get_fresh_aux_symbol(
     class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
   symbol_exprt class1=class1_sym.symbol_expr();
@@ -1551,8 +1555,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
   code.add(code_assignt(string_expr_sym1, string_expr1));
 
   // string1 = (String*) string_expr
-  pointer_typet string_ptr_type(
-    symbol_table.lookup("java::java.lang.String").type);
+  pointer_typet string_ptr_type=
+    java_reference_type(symbol_table.lookup("java::java.lang.String").type);
   exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code);
   code.add(
     code_assign_string_expr_to_new_java_string(