diff --git a/regression/ansi-c/sizeof5/test.desc b/regression/ansi-c/sizeof5/test.desc
index 466da18b2b5..0e1ed863bc1 100644
--- a/regression/ansi-c/sizeof5/test.desc
+++ b/regression/ansi-c/sizeof5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Function_Arguments1/test.desc b/regression/cbmc-cpp/Function_Arguments1/test.desc
index 91d9cf8b52e..c3e81575d7f 100644
--- a/regression/cbmc-cpp/Function_Arguments1/test.desc
+++ b/regression/cbmc-cpp/Function_Arguments1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc/null6/main.c b/regression/cbmc/null6/main.c
index ae4005d5547..bd6a95a75ce 100644
--- a/regression/cbmc/null6/main.c
+++ b/regression/cbmc/null6/main.c
@@ -1,4 +1,4 @@
-void *guard_malloc_counter = 0;
+char *guard_malloc_counter = 0;
 
 void *my_malloc(int size)
 {
diff --git a/regression/cbmc/ptr_arithmetic_on_null/test.desc b/regression/cbmc/ptr_arithmetic_on_null/test.desc
index 52a80374b32..b60f5bb3539 100644
--- a/regression/cbmc/ptr_arithmetic_on_null/test.desc
+++ b/regression/cbmc/ptr_arithmetic_on_null/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^\[main.assertion.1\] line .* assertion \(void \*\)0 != \(void \*\)0 \+ \(.*\)1: SUCCESS$
diff --git a/regression/cbmc/void_pointer1/test.desc b/regression/cbmc/void_pointer1/test.desc
index 39c491ba8bb..d5e386bad9a 100644
--- a/regression/cbmc/void_pointer1/test.desc
+++ b/regression/cbmc/void_pointer1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/void_pointer2/test.desc b/regression/cbmc/void_pointer2/test.desc
index 3556481d977..6daabc695da 100644
--- a/regression/cbmc/void_pointer2/test.desc
+++ b/regression/cbmc/void_pointer2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --pointer-check --no-simplify --unwind 3
 ^EXIT=0$
diff --git a/regression/cbmc/void_pointer3/test.desc b/regression/cbmc/void_pointer3/test.desc
index 39d9265e8a7..564e56ae192 100644
--- a/regression/cbmc/void_pointer3/test.desc
+++ b/regression/cbmc/void_pointer3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend gcc-only
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/void_pointer5/test.desc b/regression/cbmc/void_pointer5/test.desc
index 59d65ddf9f7..82341664036 100644
--- a/regression/cbmc/void_pointer5/test.desc
+++ b/regression/cbmc/void_pointer5/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend gcc-only
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/void_pointer6/test.desc b/regression/cbmc/void_pointer6/test.desc
index b32be6d64d0..503df2ca2a0 100644
--- a/regression/cbmc/void_pointer6/test.desc
+++ b/regression/cbmc/void_pointer6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/void_pointer7/test.desc b/regression/cbmc/void_pointer7/test.desc
index 626cfabcc56..3db12932134 100644
--- a/regression/cbmc/void_pointer7/test.desc
+++ b/regression/cbmc/void_pointer7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/contracts/assigns_enforce_conditional_void_target/test.desc b/regression/contracts/assigns_enforce_conditional_void_target/test.desc
index dd1dc9cb31f..14f7eb2f2ba 100644
--- a/regression/contracts/assigns_enforce_conditional_void_target/test.desc
+++ b/regression/contracts/assigns_enforce_conditional_void_target/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.* error: void-typed expressions not allowed as assigns clause targets$
+^.* error: (void-typed expressions not allowed as assigns clause targets|dereferencing void pointer)$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc
index dd1dc9cb31f..14f7eb2f2ba 100644
--- a/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc
+++ b/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.* error: void-typed expressions not allowed as assigns clause targets$
+^.* error: (void-typed expressions not allowed as assigns clause targets|dereferencing void pointer)$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_side_effects_1/test.desc b/regression/contracts/assigns_enforce_side_effects_1/test.desc
index 693bd0f8f05..5b0fe231fe9 100644
--- a/regression/contracts/assigns_enforce_side_effects_1/test.desc
+++ b/regression/contracts/assigns_enforce_side_effects_1/test.desc
@@ -1,9 +1,8 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: void-typed expressions not allowed as assigns clause targets$
-^.*error: side-effects not allowed in assigns clause targets$
-^.*error: ternary expressions not allowed in assigns clause targets$
+activate-multi-line-match
+.*error: (dereferencing void pointer|void-typed expressions not allowed as assigns clause targets\n.*\n.*error: side-effects not allowed in assigns clause targets\n.*\n.*error: ternary expressions not allowed in assigns clause targets\n)
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/goto-cl/void-pointer/main.c b/regression/goto-cl/void-pointer/main.c
new file mode 100644
index 00000000000..1bc102811ef
--- /dev/null
+++ b/regression/goto-cl/void-pointer/main.c
@@ -0,0 +1,15 @@
+void *malloc(__CPROVER_size_t);
+int printf(const char *, ...);
+
+int main(int argc, char *argv[])
+{
+  void *p = malloc(2);
+  printf("%p\n", p);
+#ifdef VOID1
+  (void)*p;
+#else
+  void *q = &p[1];
+  printf("%p\n", q);
+#endif
+  return 0;
+}
diff --git a/regression/goto-cl/void-pointer/ptr-arithmetic.desc b/regression/goto-cl/void-pointer/ptr-arithmetic.desc
new file mode 100644
index 00000000000..1b3ce37bae3
--- /dev/null
+++ b/regression/goto-cl/void-pointer/ptr-arithmetic.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+error: pointer arithmetic with unknown object size
+^CONVERSION ERROR$
+^EXIT=(64|1)$
+^SIGNAL=0$
+--
+Invariant check failed
diff --git a/regression/goto-cl/void-pointer/test.desc b/regression/goto-cl/void-pointer/test.desc
new file mode 100644
index 00000000000..8107c8a08bd
--- /dev/null
+++ b/regression/goto-cl/void-pointer/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+-DVOID1
+error: dereferencing void pointer
+^CONVERSION ERROR$
+^EXIT=(64|1)$
+^SIGNAL=0$
+--
+Invariant check failed
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index e40c3b7a878..39bb04eb20f 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -1784,6 +1784,15 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
   else if(op_type.id()==ID_pointer)
   {
     expr.type() = to_pointer_type(op_type).base_type();
+
+    if(
+      expr.type().id() == ID_empty &&
+      config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)
+    {
+      error().source_location = expr.source_location();
+      error() << "dereferencing void pointer" << eom;
+      throw 0;
+    }
   }
   else
   {
@@ -3718,6 +3727,14 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
     error() << "pointer arithmetic with unknown object size" << eom;
     throw 0;
   }
+  else if(
+    base_type.id() == ID_empty &&
+    config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)
+  {
+    error().source_location = expr.source_location();
+    error() << "pointer arithmetic with unknown object size" << eom;
+    throw 0;
+  }
 }
 
 void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)