Visual Studio rejects pointer arithmetic and dereferencing of void*

tautschnig · tautschnig · commit 674a8f03ac6b · 2022-02-16T16:10:58.000Z
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
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE gcc-only`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-void *guard_malloc_counter = 0;`
	`1`	`+char *guard_malloc_counter = 0;`
`2`	`2`
`3`	`3`	`void *my_malloc(int size)`
`4`	`4`	`{`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE broken-smt-backend gcc-only`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`