Merge pull request #4102 from tautschnig/remove-void_typet

Remove void_typet

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1225,7 +1225,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     if(statement=="aconst_null")
     {
       assert(results.size()==1);
-      results[0]=null_pointer_exprt(java_reference_type(void_typet()));
+      results[0] = null_pointer_exprt(java_reference_type(java_void_type()));
     }
     else if(statement=="athrow")
     {
@@ -1349,7 +1349,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
         from_integer(
           std::next(i_it)->address,
           unsignedbv_typet(64));
-      results[0].type()=pointer_type(void_typet());
+      results[0].type() = pointer_type(java_void_type());
     }
     else if(statement=="ret")
     {
@@ -1981,8 +1981,8 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
 
   // becomes a function call
   java_method_typet type(
-    {java_method_typet::parametert(java_reference_type(void_typet()))},
-    void_typet());
+    {java_method_typet::parametert(java_reference_type(java_void_type()))},
+    java_void_type());
   code_function_callt call(symbol_exprt(descriptor, type), {op[0]});
   call.add_source_location() = source_location;
   if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
@@ -2725,7 +2725,7 @@ code_ifthenelset java_bytecode_convert_methodt::convert_ifnull(
   const mp_integer &number,
   const source_locationt &location) const
 {
-  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
+  const typecast_exprt lhs(op[0], java_reference_type(java_void_type()));
   const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
 
   const method_offsett label_number = numeric_cast_v<method_offsett>(number);
@@ -2747,7 +2747,7 @@ code_ifthenelset java_bytecode_convert_methodt::convert_ifnonull(
   const mp_integer &number,
   const source_locationt &location) const
 {
-  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
+  const typecast_exprt lhs(op[0], java_reference_type(java_void_type()));
   const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
 
   const method_offsett label_number = numeric_cast_v<method_offsett>(number);
@@ -2830,7 +2830,7 @@ code_blockt java_bytecode_convert_methodt::convert_ret(
     {
       auto address_ptr =
         from_integer(jsr_ret_targets[idx], unsignedbv_typet(64));
-      address_ptr.type() = pointer_type(void_typet());
+      address_ptr.type() = pointer_type(java_void_type());
 
       code_ifthenelset branch(equal_exprt(retvar, address_ptr), std::move(g));
 

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -224,7 +224,7 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
   binary_predicate_exprt class_cast_check(
     class1, ID_java_instanceof, class2);
 
-  pointer_typet voidptr=pointer_type(empty_typet());
+  pointer_typet voidptr = pointer_type(java_void_type());
   exprt null_check_op=class1;
   if(null_check_op.type()!=voidptr)
     null_check_op.make_typecast(voidptr);

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_internal_additions.h"
 
 // For INFLIGHT_EXCEPTION_VARIABLE_NAME
+#include "java_types.h"
 #include "remove_exceptions.h"
 
 #include <util/std_types.h>
@@ -37,7 +38,7 @@ void java_internal_additions(symbol_table_baset &dest)
     symbolt symbol;
     symbol.base_name = CPROVER_PREFIX "malloc_object";
     symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type=pointer_type(empty_typet());
+    symbol.type = pointer_type(java_void_type());
     symbol.mode=ID_C;
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
@@ -50,7 +51,7 @@ void java_internal_additions(symbol_table_baset &dest)
     symbol.base_name = INFLIGHT_EXCEPTION_VARIABLE_BASENAME;
     symbol.name = INFLIGHT_EXCEPTION_VARIABLE_NAME;
     symbol.mode = ID_java;
-    symbol.type = pointer_type(empty_typet());
+    symbol.type = pointer_type(java_void_type());
     symbol.type.set(ID_C_no_nondet_initialization, true);
     symbol.value = null_pointer_exprt(to_pointer_type(symbol.type));
     symbol.is_file_local = false;

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -38,7 +38,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
   initialize.base_name=INITIALIZE_FUNCTION;
   initialize.mode=ID_java;
 
-  initialize.type = java_method_typet({}, empty_typet());
+  initialize.type = java_method_typet({}, java_void_type());
 
   code_blockt init_code;
 
@@ -225,7 +225,7 @@ static void java_static_lifetime_init(
         // Then call the init function:
         code_block.add(std::move(initializer_call));
       }
-      else if(sym.value.is_nil() && sym.type!=empty_typet())
+      else if(sym.value.is_nil() && sym.type != java_void_type())
       {
         const bool is_class_model =
           has_suffix(id2string(sym.name), "@class_model");
@@ -446,7 +446,7 @@ void java_record_outputs(
   result.reserve(parameters.size()+1);
 
   bool has_return_value =
-    to_java_method_type(function.type).return_type() != empty_typet();
+    to_java_method_type(function.type).return_type() != java_void_type();
 
   if(has_return_value)
   {
@@ -702,7 +702,7 @@ bool generate_java_start_function(
 
   // if the method return type is not void, store return value in a new variable
   // named 'return'
-  if(to_java_method_type(symbol.type).return_type() != empty_typet())
+  if(to_java_method_type(symbol.type).return_type() != java_void_type())
   {
     auxiliary_symbolt return_symbol;
     return_symbol.mode=ID_java;
@@ -720,7 +720,7 @@ bool generate_java_start_function(
   exc_symbol.mode=ID_java;
   exc_symbol.name=JAVA_ENTRY_POINT_EXCEPTION_SYMBOL;
   exc_symbol.base_name=exc_symbol.name;
-  exc_symbol.type=java_reference_type(empty_typet());
+  exc_symbol.type = java_reference_type(java_void_type());
   symbol_table.add(exc_symbol);
 
   // Zero-initialise the top-level exception catch variable:
@@ -792,7 +792,7 @@ bool generate_java_start_function(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type = java_method_typet({}, empty_typet());
+  new_symbol.type = java_method_typet({}, java_void_type());
   new_symbol.value.swap(init_code);
   new_symbol.mode=ID_java;
 

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -592,7 +592,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   // If this is a void* we *must* initialise with null:
   // (This can currently happen for some cases of #exception_value)
-  bool must_be_null = subtype == empty_typet();
+  bool must_be_null = subtype == java_void_type();
 
   // If we may be about to initialize a non-null enum type, always run the
   // clinit_wrapper of its class first.

jbmc/src/java_bytecode/java_pointer_casts.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/namespace.h>
 
+#include "java_types.h"
+
 /// dereference pointer expression
 /// \return dereferenced pointer
 static exprt clean_deref(const exprt &ptr)
@@ -94,8 +96,9 @@ exprt make_clean_pointer_cast(
   if(ptr.type()==target_type)
     return ptr;
 
-  if(ptr.type().subtype()==empty_typet() ||
-     target_type.subtype()==empty_typet())
+  if(
+    ptr.type().subtype() == java_void_type() ||
+    target_type.subtype() == java_void_type())
     return typecast_exprt(ptr, target_type);
 
   const typet &target_base=ns.follow(target_type.subtype());
@@ -106,7 +109,7 @@ exprt make_clean_pointer_cast(
     assert(
       bare_ptr.type().id()==ID_pointer &&
       "Non-pointer in make_clean_pointer_cast?");
-    if(bare_ptr.type().subtype()==empty_typet())
+    if(bare_ptr.type().subtype() == java_void_type())
       bare_ptr=bare_ptr.op0();
   }
 

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -352,7 +352,7 @@ static void create_clinit_wrapper_symbols(
 
   // Create symbol for the "clinit_wrapper"
   symbolt wrapper_method_symbol;
-  const java_method_typet wrapper_method_type({}, void_typet());
+  const java_method_typet wrapper_method_type({}, java_void_type());
   wrapper_method_symbol.name = clinit_wrapper_name(class_name);
   wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
   wrapper_method_symbol.base_name = "clinit_wrapper";
@@ -790,7 +790,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
       "a class cannot be both incomplete, and so have stub static fields, and "
       "also define a static initializer");
 
-    const java_method_typet thunk_type({}, void_typet());
+    const java_method_typet thunk_type({}, java_void_type());
 
     symbolt static_init_symbol;
     static_init_symbol.name = static_init_name;

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1291,7 +1291,7 @@ dereference_exprt java_string_library_preprocesst::get_object_at_index(
   std::size_t index)
 {
   dereference_exprt deref_objs(argv, argv.type().subtype());
-  pointer_typet empty_pointer=pointer_type(empty_typet());
+  pointer_typet empty_pointer = pointer_type(java_void_type());
   pointer_typet pointer_of_pointer=pointer_type(empty_pointer);
   member_exprt data_member(deref_objs, "data", pointer_of_pointer);
   plus_exprt data_pointer_plus_index(

jbmc/src/java_bytecode/java_types.cpp

@@ -35,9 +35,9 @@ signedbv_typet java_int_type()
   return result;
 }
 
-void_typet java_void_type()
+empty_typet java_void_type()
 {
-  static const auto result = void_typet();
+  static const auto result = empty_typet();
   return result;
 }
 
@@ -209,7 +209,8 @@ typet java_type_from_char(char t)
   case 'f': return java_float_type();
   case 'd': return java_double_type();
   case 'z': return java_boolean_type();
-  case 'a': return java_reference_type(void_typet());
+  case 'a':
+    return java_reference_type(java_void_type());
   default:
     UNREACHABLE;
   }

jbmc/src/java_bytecode/java_types.h

@@ -368,7 +368,7 @@ unsignedbv_typet java_char_type();
 floatbv_typet java_float_type();
 floatbv_typet java_double_type();
 c_bool_typet java_boolean_type();
-void_typet java_void_type();
+empty_typet java_void_type();
 reference_typet java_reference_type(const typet &subtype);
 reference_typet java_lang_object_type();
 struct_tag_typet java_classname(const std::string &);

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -30,6 +30,8 @@ Date:   December 2016
 
 #include <analyses/uncaught_exceptions_analysis.h>
 
+#include "java_types.h"
+
 /// Lowers high-level exception descriptions into low-level operations suitable
 /// for symex and other analyses that don't understand the THROW or CATCH GOTO
 /// instructions.
@@ -228,7 +230,7 @@ void remove_exceptionst::instrument_exception_handler(
     const symbol_exprt thrown_global_symbol=
       get_inflight_exception_global();
     // next we reset the exceptional return to NULL
-    null_pointer_exprt null_voidptr((pointer_type(empty_typet())));
+    null_pointer_exprt null_voidptr((pointer_type(java_void_type())));
 
     // add the assignment @inflight_exception = NULL
     goto_programt::targett t_null=goto_program.insert_after(instr_it);
@@ -443,7 +445,7 @@ bool remove_exceptionst::instrument_function_call(
   {
     equal_exprt no_exception_currently_in_flight(
       get_inflight_exception_global(),
-      null_pointer_exprt(pointer_type(empty_typet())));
+      null_pointer_exprt(pointer_type(java_void_type())));
 
     if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
     {

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -187,7 +187,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
   else
   {
     const typet &required_return_type = required_type.return_type();
-    if(required_return_type != empty_typet())
+    if(required_return_type != java_void_type())
     {
       symbolt &to_return_symbol = get_fresh_aux_symbol(
         required_return_type,

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp

@@ -139,7 +139,7 @@ SCENARIO(
         const auto &id =
           to_symbol_expr(element_value_pair.value).get_identifier();
         const auto &java_type = java_type_from_string(id2string(id));
-        REQUIRE(*java_type == void_type());
+        REQUIRE(*java_type == java_void_type());
       }
     }
     WHEN("Parsing an annotation with an array field.")

regression/invariants/driver.cpp

@@ -118,7 +118,7 @@ int main(int argc, char** argv)
   else if(arg=="data-invariant-string")
     DATA_INVARIANT(false, "Test invariant failure");
   else if(arg=="irep")
-    INVARIANT_WITH_IREP(false, "error with irep", pointer_type(void_typet()));
+    INVARIANT_WITH_IREP(false, "error with irep", pointer_type(empty_typet()));
   else if(arg == "invariant-diagnostics")
     INVARIANT_WITH_DIAGNOSTICS(
       false,

src/ansi-c/ansi_c_entry_point.cpp

@@ -54,8 +54,8 @@ void record_function_outputs(
   code_blockt &init_code,
   symbol_tablet &symbol_table)
 {
-  bool has_return_value=
-    to_code_type(function.type).return_type()!=empty_typet();
+  bool has_return_value =
+    to_code_type(function.type).return_type() != void_type();
 
   if(has_return_value)
   {
@@ -232,7 +232,7 @@ bool generate_ansi_c_start_function(
   call_main.add_source_location()=symbol.location;
   call_main.function().add_source_location()=symbol.location;
 
-  if(to_code_type(symbol.type).return_type()!=empty_typet())
+  if(to_code_type(symbol.type).return_type() != void_type())
   {
     auxiliary_symbolt return_symbol;
     return_symbol.mode=ID_C;
@@ -515,7 +515,7 @@ bool generate_ansi_c_start_function(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type = code_typet({}, empty_typet());
+  new_symbol.type = code_typet({}, void_type());
   new_symbol.value.swap(init_code);
   new_symbol.mode=symbol.mode;
 

src/ansi-c/c_typecheck_base.cpp

@@ -11,10 +11,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_typecheck_base.h"
 
+#include <util/c_types.h>
+#include <util/config.h>
 #include <util/invariant.h>
-#include <util/std_types.h>
 #include <util/prefix.h>
-#include <util/config.h>
+#include <util/std_types.h>
 
 #include "expr2c.h"
 #include "type2name.h"
@@ -740,7 +741,7 @@ void c_typecheck_baset::typecheck_declaration(
 
       typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
 
-      typet ret_type=empty_typet();
+      typet ret_type = void_type();
       if(new_symbol.type.id()==ID_code)
         ret_type=to_code_type(new_symbol.type).return_type();
       assert(parameter_map.empty());

src/ansi-c/c_typecheck_code.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_typecheck_base.h"
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_initializer.h>
 
@@ -575,7 +576,7 @@ void c_typecheck_baset::typecheck_gcc_computed_goto(codet &code)
   assert(dest.operands().size()==1);
 
   typecheck_expr(dest.op0());
-  dest.type()=empty_typet();
+  dest.type() = void_type();
 }
 
 void c_typecheck_baset::typecheck_ifthenelse(code_ifthenelset &code)

src/ansi-c/c_typecheck_expr.cpp

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

src/ansi-c/parser_static.inc

@@ -82,7 +82,6 @@ Function: statement
 static void statement(YYSTYPE &expr, const irep_idt &id)
 {
   set(expr, ID_code);
-  stack(expr).type().id(ID_code);
   stack(expr).set(ID_statement, id);
 }