From b8f648300d56292e52b0515dd88bb28b8e78f14e Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Mon, 20 Jul 2020 09:13:30 +0100
Subject: [PATCH] Fix cbmc crash on pointer checks of void pointer dereferences

---
 regression/cbmc/void_pointer6/main.c    |  5 +++++
 regression/cbmc/void_pointer6/test.desc | 10 ++++++++++
 regression/cbmc/void_pointer7/main.c    |  6 ++++++
 regression/cbmc/void_pointer7/test.desc | 11 +++++++++++
 src/analyses/goto_check.cpp             | 20 +++++++++++++++++---
 5 files changed, 49 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc/void_pointer6/main.c
 create mode 100644 regression/cbmc/void_pointer6/test.desc
 create mode 100644 regression/cbmc/void_pointer7/main.c
 create mode 100644 regression/cbmc/void_pointer7/test.desc

diff --git a/regression/cbmc/void_pointer6/main.c b/regression/cbmc/void_pointer6/main.c
new file mode 100644
index 00000000000..2992549870c
--- /dev/null
+++ b/regression/cbmc/void_pointer6/main.c
@@ -0,0 +1,5 @@
+int main()
+{
+  void *p;
+  *p;
+}
diff --git a/regression/cbmc/void_pointer6/test.desc b/regression/cbmc/void_pointer6/test.desc
new file mode 100644
index 00000000000..b32be6d64d0
--- /dev/null
+++ b/regression/cbmc/void_pointer6/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Checks that cbmc does not crash with --pointer-check on dereference of an
+invalid void pointer
diff --git a/regression/cbmc/void_pointer7/main.c b/regression/cbmc/void_pointer7/main.c
new file mode 100644
index 00000000000..1a823faf56b
--- /dev/null
+++ b/regression/cbmc/void_pointer7/main.c
@@ -0,0 +1,6 @@
+int main()
+{
+  int a = 0;
+  void *p = &a;
+  *p;
+}
diff --git a/regression/cbmc/void_pointer7/test.desc b/regression/cbmc/void_pointer7/test.desc
new file mode 100644
index 00000000000..626cfabcc56
--- /dev/null
+++ b/regression/cbmc/void_pointer7/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Checks that cbmc does not crash with --pointer-check on dereference of a valid
+void pointer
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index aaf277a904f..bd81d06dae6 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1164,10 +1164,24 @@ void goto_checkt::pointer_validity_check(
 
   const exprt &pointer=expr.pointer();
 
-  auto size_of_expr_opt = size_of_expr(expr.type(), ns);
-  CHECK_RETURN(size_of_expr_opt.has_value());
+  exprt size;
 
-  auto conditions = address_check(pointer, size_of_expr_opt.value());
+  if(expr.type().id() == ID_empty)
+  {
+    // a dereference *p (with p being a pointer to void) is valid if p points to
+    // valid memory (of any size). the smallest possible size of the memory
+    // segment p could be pointing to is 1, hence we use this size for the
+    // address check
+    size = from_integer(1, size_type());
+  }
+  else
+  {
+    auto size_of_expr_opt = size_of_expr(expr.type(), ns);
+    CHECK_RETURN(size_of_expr_opt.has_value());
+    size = size_of_expr_opt.value();
+  }
+
+  auto conditions = address_check(pointer, size);
 
   for(const auto &c : conditions)
   {