diff --git a/regression/goto-instrument-unused/Makefile b/regression/goto-instrument-unused/Makefile
new file mode 100644
index 00000000000..2379cc78ca3
--- /dev/null
+++ b/regression/goto-instrument-unused/Makefile
@@ -0,0 +1,21 @@
+default: tests.log
+
+test:
+	@../test.pl -c ../run.sh
+
+tests.log: ../test.pl
+	@../test.pl -c ../run.sh
+
+clean:
+	@for dir in *; do \
+                if [ -d "$$dir" ]; then \
+                        rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
+                fi; \
+        done;
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
diff --git a/regression/goto-instrument-unused/global-unused/main.c b/regression/goto-instrument-unused/global-unused/main.c
new file mode 100644
index 00000000000..6368de7f138
--- /dev/null
+++ b/regression/goto-instrument-unused/global-unused/main.c
@@ -0,0 +1,67 @@
+#include <stdio.h>
+
+int a = 2; // unused
+char b;
+unsigned long int c;
+unsigned char d; // write only
+int e = 9;       // used in return statement
+
+int usedi = 100;
+
+struct
+{
+  int data;
+} s_unused, s_writeonly, s_used;
+
+unsigned long int f()
+{
+  usedi = usedi + 1;
+  unsigned long int *p_f = &c; // uses as read
+  return *p_f;
+}
+
+int *g()
+{
+  usedi = usedi + 2;
+  return &e; // uses e, but return value of g is used in write only
+}
+
+int h()
+{
+  return s_used.data;
+}
+
+unsigned long int i()
+{
+  return c = d + e;
+}
+
+int main()
+{
+  int p_a = 5; // unused
+  unsigned long int p_b = f();
+  int *p_c = g(); // unused
+  int p_d = 6;
+  int p_e = 7;
+  int p_f = 8;
+  int *p_g = g();
+  i();
+
+  s_used.data = 0;
+  s_writeonly = s_used;
+
+  d = p_b + 9;
+  printf("%d\n", p_d);
+  printf("%p\n", &p_e);
+  printf("%d\n", s_used.data);
+  printf("%d\n", *p_g);
+  printf("%d\n", h());
+  if(p_f)
+  {
+    return 0;
+  }
+  else
+  {
+    return 1;
+  }
+}
diff --git a/regression/goto-instrument-unused/global-unused/test.desc b/regression/goto-instrument-unused/global-unused/test.desc
new file mode 100644
index 00000000000..7c855f02ed3
--- /dev/null
+++ b/regression/goto-instrument-unused/global-unused/test.desc
@@ -0,0 +1,21 @@
+CORE
+main.c
+0
+^SIGNAL=0$
+main.c:35 variable p_c is never read
+main.c:4 variable b is never read
+main.c:3 variable a is never read
+main.c:11 variable s_writeonly is never read
+main.c:33 variable p_a is never read
+main.c:11 variable s_unused is never read
+--
+main.c:9 variable usedi is never read
+main.c:34 variable p_b is never read
+main.c:11 variable s_used is never read
+main.c:39 variable p_g is never read
+main.c:15 variable p_f is never read
+main.c:6 variable d is never read
+main.c:38 variable p_f is never read
+main.c:50 variable return_value_h$1 is never read
+main.c:36 variable p_d is never read
+^warning: ignoring
diff --git a/regression/goto-instrument-unused/mmap/main.c b/regression/goto-instrument-unused/mmap/main.c
new file mode 100644
index 00000000000..23dd143835b
--- /dev/null
+++ b/regression/goto-instrument-unused/mmap/main.c
@@ -0,0 +1,37 @@
+#include <inttypes.h>
+#include <stdio.h>
+#include <sys/mman.h>
+
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <sys/types.h>
+
+void *mapmem(off_t offset, size_t length)
+{
+  int fd;
+  uint8_t *mem, *tmp;
+  const int prot = PROT_READ | PROT_WRITE;
+  const int flags = MAP_SHARED;
+
+  mem = NULL;
+  fd = open("/dev/mem", O_RDWR | O_CLOEXEC);
+  if(fd == -1)
+    goto out;
+
+  tmp = mmap(NULL, length, prot, flags, fd, offset);
+  close(fd);
+  if(tmp == MAP_FAILED)
+    goto out;
+  mem = tmp;
+out:
+  return mem;
+}
+
+int main()
+{
+  unsigned int target = 0xffffff;
+  uint8_t *mem;
+  mem = mapmem(target, 1024L);
+  printf("got address %p from target %p\n", mem, (unsigned int *)target);
+  return 0;
+}
diff --git a/regression/goto-instrument-unused/mmap/test.desc b/regression/goto-instrument-unused/mmap/test.desc
new file mode 100644
index 00000000000..4303addfab6
--- /dev/null
+++ b/regression/goto-instrument-unused/mmap/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+0
+^SIGNAL=0$
+--
+mmap/main.c:12 variable mem is never read
+mmap/main.c:33 variable mem is never read
+mmap/main.c:21 variable return_value_mmap$1 is never rea
+mmap/main.c:34 variable return_value_mapmem$1 is never read
+mmap/main.c:9 variable offset is never read
+mmap/main.c:9 variable length is never read
+mmap/main.c:32 variable target is never read
+mmap/main.c:11 variable fd is never read
+mmap/main.c:14 variable flags is never read
+mmap/main.c:13 variable prot is never read
+mmap/main.c:12 variable tmp is never read
diff --git a/regression/goto-instrument-unused/run.sh b/regression/goto-instrument-unused/run.sh
new file mode 100755
index 00000000000..3740cfa8986
--- /dev/null
+++ b/regression/goto-instrument-unused/run.sh
@@ -0,0 +1,6 @@
+# compile test case
+# to be called from sub-directories only, to match path to tools
+../../../src/goto-cc/goto-cc main.c -o test &> /dev/null; echo $?
+
+../../../src/goto-instrument/goto-instrument --show-unused test
+echo $?
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index eb67f14f140..207357ee39e 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -54,6 +54,7 @@ SRC = accelerate/accelerate.cpp \
       remove_function.cpp \
       rw_set.cpp \
       show_locations.cpp \
+      show_unused.cpp \
       skip_loops.cpp \
       splice_call.cpp \
       stack_depth.cpp \
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index fd9a511eeb4..d8fb0a940af 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -100,6 +100,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "undefined_functions.h"
 #include "remove_function.h"
 #include "splice_call.h"
+#include "show_unused.h"
 
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()
@@ -438,6 +439,13 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
+    if(cmdline.isset("show-unused"))
+    {
+      do_indirect_call_and_rtti_removal();
+      show_unused(get_ui(), goto_model);
+      return CPROVER_EXIT_SUCCESS;
+    }
+
     if(cmdline.isset("show-rw-set"))
     {
       namespacet ns(goto_model.symbol_table);
@@ -1494,6 +1502,8 @@ void goto_instrument_parse_optionst::help()
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     " --print-internal-representation\n" // NOLINTNEXTLINE(*)
     "                              show verbose internal representation of the program\n"
+    " --show-unused                list variables that are never read\n"
+    " --show-goto-functions        show goto program\n"
     " --list-undefined-functions   list functions without body\n"
     " --show-struct-alignment      show struct members that might be concurrently accessed\n" // NOLINT(*)
     " --show-natural-loops         show natural loop heads\n"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index dd6950932e4..d1f2d72d847 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -74,7 +74,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(print-internal-representation)" \
   "(remove-function-pointers)" \
   "(show-claims)(property):" \
-  "(show-symbol-table)(show-points-to)(show-rw-set)" \
+  "(show-symbol-table)(show-points-to)(show-rw-set)(show-unused)" \
   "(cav11)" \
   OPT_TIMESTAMP \
   "(show-natural-loops)(accelerate)(havoc-loops)" \
diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp
index d6a2380dd78..abc7267564c 100644
--- a/src/goto-instrument/rw_set.cpp
+++ b/src/goto-instrument/rw_set.cpp
@@ -51,6 +51,10 @@ void _rw_set_loct::compute()
     assert(target->code.operands().size()==2);
     assign(target->code.op0(), target->code.op1());
   }
+  else if(target->is_return())
+  {
+    read(to_code_return(target->code));
+  }
   else if(target->is_goto() ||
           target->is_assume() ||
           target->is_assert())
@@ -74,6 +78,10 @@ void _rw_set_loct::compute()
     if(code_function_call.lhs().is_not_nil())
       write(code_function_call.lhs());
   }
+  else if(target->is_other())
+  {
+    read(target->code);
+  }
 }
 
 void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)
diff --git a/src/goto-instrument/show_unused.cpp b/src/goto-instrument/show_unused.cpp
new file mode 100644
index 00000000000..86f73aa1dda
--- /dev/null
+++ b/src/goto-instrument/show_unused.cpp
@@ -0,0 +1,114 @@
+/*******************************************************************\
+
+Module: Show unused variables (including write only)
+
+Author: Norbert Manthey nmanthey@iamazon.com
+
+\*******************************************************************/
+
+#include <cassert>
+#include <iostream>
+
+#include <util/file_util.h>
+#include <util/prefix.h>
+
+#include <analyses/dirty.h>
+#include <goto-instrument/rw_set.h>
+#include <pointer-analysis/value_set_analysis_fi.h>
+
+#include "show_unused.h"
+
+/*******************************************************************\
+
+Function: show_unused
+
+  Inputs: symbol table, goto program
+
+ Outputs: prints list of variables that are never read
+          returns false, if no unused variables have been found,
+          else true
+
+ Purpose: help to spot variables that are never used globally in a
+          program
+
+\*******************************************************************/
+
+bool show_unused(ui_message_handlert::uit ui, const goto_modelt &goto_model)
+{
+  const symbol_tablet &symbol_table = goto_model.symbol_table;
+  const goto_functionst &goto_functions = goto_model.goto_functions;
+  const namespacet ns(symbol_table);
+  rw_set_baset global_reads(ns);
+
+  // get all symbols whose address is used
+  dirtyt dirty_symbols(goto_functions);
+
+  // compute for each function the set of read and written symbols
+  forall_goto_functions(it, goto_functions)
+  {
+    if(!it->second.body_available())
+      continue;
+
+    if(!symbol_table.has_symbol(it->first))
+    {
+      std::cerr << " warning: did not find symbol for: " << id2string(it->first)
+                << std::endl;
+      continue;
+    }
+    const symbolt *symbol = symbol_table.lookup(it->first);
+
+    value_set_analysis_fit value_sets(ns);
+    rw_set_functiont rw_set(value_sets, goto_model, symbol->symbol_expr());
+    global_reads += rw_set;
+  }
+
+  // check the symbol table against the global_reads set, collect unused symbols
+  std::vector<std::pair<const irep_idt, symbolt>> actual_unused_symbols;
+  // forall_symbols(it, symbol_table.symbols)
+  for(const auto symbol_pair : symbol_table.symbols)
+  {
+    // we are not interested in functions that are not read
+    if(symbol_pair.second.type.id() == ID_code)
+      continue;
+
+    // skip internal, anonymous symbols, and if no location is present
+    if(has_prefix(id2string(symbol_pair.second.name), "__CPROVER"))
+      continue;
+    if(has_prefix(id2string(symbol_pair.second.base_name), "#anon"))
+      continue;
+    if(symbol_pair.second.location.as_string().empty())
+      continue;
+
+    if(
+      !global_reads.has_r_entry(symbol_pair.second.name) &&
+      dirty_symbols.get_dirty_ids().find(symbol_pair.second.name) ==
+        dirty_symbols.get_dirty_ids().end())
+    {
+      actual_unused_symbols.push_back(symbol_pair);
+    }
+  }
+
+  // print collected symbols
+  switch(ui)
+  {
+  case ui_message_handlert::uit::PLAIN:
+    std::cerr << "found " << actual_unused_symbols.size()
+              << " symbols to report" << std::endl;
+    for(auto it = actual_unused_symbols.begin();
+        it != actual_unused_symbols.end();
+        ++it)
+    {
+      const source_locationt &location = it->second.location;
+      std::cout << concat_dir_file(
+                     id2string(location.get_working_directory()),
+                     id2string(location.get_file()))
+                << ":" << id2string(location.get_line()) << " variable "
+                << id2string(it->second.base_name) << " is never read"
+                << std::endl;
+    }
+    break;
+  default:
+    assert(false && "chosen UI is not yet implemented");
+  }
+  return 0;
+}
diff --git a/src/goto-instrument/show_unused.h b/src/goto-instrument/show_unused.h
new file mode 100644
index 00000000000..82fc290dc11
--- /dev/null
+++ b/src/goto-instrument/show_unused.h
@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Show unused variables (including write only)
+
+Author: Norbert Manthey nmanthey@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_INSTRUMENT_SHOW_UNUSED_H
+#define CPROVER_GOTO_INSTRUMENT_SHOW_UNUSED_H
+
+#include <util/ui_message.h>
+
+#include <goto-programs/goto_model.h>
+
+class symbol_tablet;
+
+/** display all variables that are never read in the program */
+bool show_unused(ui_message_handlert::uit ui, const goto_modelt &goto_model);
+
+#endif
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index a69432ce316..41e17ff23f6 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -340,6 +340,9 @@ void objects_read(
   else if(src.id()==ID_address_of)
   {
     // don't traverse!
+    assert(src.operands().size() == 1);
+    dest.push_back(src);
+    objects_read(src.op0(), dest);
   }
   else if(src.id()==ID_dereference)
   {
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 422a492896e..e094544d32d 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -933,12 +933,18 @@ template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
 inline const code_returnt &to_code_return(const codet &code)
 {
   assert(code.get_statement()==ID_return);
+  assert(
+    code.operands().size() <= 1 &&
+    "there should be at most one operand in an return statement");
   return static_cast<const code_returnt &>(code);
 }
 
 inline code_returnt &to_code_return(codet &code)
 {
   assert(code.get_statement()==ID_return);
+  assert(
+    code.operands().size() <= 1 &&
+    "there should be at most one operand in an return statement");
   return static_cast<code_returnt &>(code);
 }