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/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