Merge pull request #7605 from tautschnig/bugfixes/fpr-nil

Function-pointer removal: fix interaction with slice-global-inits

Author: tautschnig

regression/goto-instrument/slice-global-inits5/main.c

@@ -0,0 +1,15 @@
+int foo(void)
+{
+}
+
+const int (*const fptrs[])(void) = {&foo};
+
+void unused()
+{
+  const int (*const fp)(void) = fptrs[0];
+  (*fp)();
+}
+
+int main()
+{
+}

regression/goto-instrument/slice-global-inits5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--remove-function-pointers --slice-global-inits
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-instrument/slice-global-inits6/main.c

@@ -0,0 +1,9 @@
+int foo()
+{
+}
+
+int main()
+{
+  int (*fp)() = &foo;
+  (*fp)();
+}

regression/goto-instrument/slice-global-inits6/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--slice-global-inits
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1481,6 +1481,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("slice-global-inits"))
   {
+    do_indirect_call_and_rtti_removal();
+
     log.status() << "Slicing away initializations of unused global variables"
                  << messaget::eom;
     slice_global_inits(goto_model, ui_message_handler);

src/goto-programs/remove_const_function_pointers.cpp

@@ -74,7 +74,7 @@ exprt remove_const_function_pointerst::replace_const_symbols(
     {
       const symbolt &symbol =
         symbol_table.lookup_ref(to_symbol_expr(expression).get_identifier());
-      if(symbol.type.id()!=ID_code)
+      if(symbol.type.id() != ID_code && symbol.value.is_not_nil())
       {
         const exprt &symbol_value=symbol.value;
         return replace_const_symbols(symbol_value);