Visual Studio rejects pointer arithmetic and dereferencing of void*

Pointer arithmetic using void* is a (document) GCC extension.
Dereferencing void* pointers is permitted by GCC when the value is
unused. Visual Studio rejects both.

This required updates to tests to either not rely on pointer arithmetic
over void*, or restrict tests to GCC only.

Fixes: #5275

Author: tautschnig

regression/ansi-c/sizeof5/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/cbmc/null6/main.c

@@ -1,4 +1,4 @@
-void *guard_malloc_counter = 0;
+char *guard_malloc_counter = 0;
 
 void *my_malloc(int size)
 {

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$

regression/cbmc/void_pointer1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/void_pointer2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --pointer-check --no-simplify --unwind 3
 ^EXIT=0$

regression/cbmc/void_pointer3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend gcc-only
 main.c
 
 ^EXIT=0$

regression/cbmc/void_pointer5/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend gcc-only
 main.c
 
 ^EXIT=10$

regression/cbmc/void_pointer6/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/void_pointer7/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 --pointer-check
 ^EXIT=0$

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;
+}

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

regression/goto-cl/void-pointer/test-global.desc

@@ -0,0 +1,9 @@
+CORE test-c++-front-end
+main.c
+-Dvoid_global
+^EXIT=(64|1)$
+^SIGNAL=0$
+void-typed symbol not permitted
+^CONVERSION ERROR$
+--
+Invariant check failed

regression/goto-cl/void-pointer/test-non-member.desc

@@ -0,0 +1,9 @@
+CORE test-c++-front-end
+main.c
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+void-typed symbol not permitted
+^CONVERSION ERROR$
+--
+Invariant check failed

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

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)