Merge pull request #6674 from tautschnig/bugfixes/5275-void-indexing

Visual Studio rejects pointer arithmetic and dereferencing of void*

Author: tautschnig

regression/ansi-c/sizeof5/test.desc

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

regression/cbmc-cpp/Function_Arguments1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.cpp
 
 ^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/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$

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$

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$

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.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)