Merge pull request #955 from tautschnig/void-cast

Properly handle void*

Author: Daniel Kroening

regression/cbmc/void_pointer1/main.c

@@ -0,0 +1,12 @@
+char buffer[2];
+int length = 2;
+
+void func(void* buf, int len)
+{
+  while( len-- )
+    *(char *)buf++;
+}
+
+void main(){
+  func(buffer,length);
+}

regression/cbmc/void_pointer1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/void_pointer2/main.c

@@ -0,0 +1,12 @@
+char buffer[2];
+int length = 2;
+
+void func(void* buf, int len)
+{
+  while( len-- )
+    *(char *)buf++;
+}
+
+void main(){
+  func(buffer,length);
+}

regression/cbmc/void_pointer2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --no-simplify --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -1238,7 +1238,8 @@ void goto_checkt::bounds_check(
     plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
 
     assert(effective_offset.op0().type()==effective_offset.op1().type());
-    assert(effective_offset.type()==size.type());
+    if(effective_offset.type()!=size.type())
+      size.make_typecast(effective_offset.type());
 
     binary_relation_exprt inequality(effective_offset, ID_lt, size);
 

src/analyses/goto_rw.cpp

@@ -149,6 +149,7 @@ void rw_range_sett::get_objects_complex(
 
   range_spect sub_size=
     to_range_spect(pointer_offset_bits(op.type().subtype(), ns));
+  assert(sub_size>0);
   range_spect offset=
     (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
 

src/analyses/invariant_set.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/base_type.h>
 #include <util/std_types.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 #include "invariant_set.h"

src/analyses/local_bitvector_analysis.cpp

@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/expr_util.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 #include "local_bitvector_analysis.h"

src/analyses/local_cfg.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/expr_util.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 #endif

src/analyses/local_may_alias.cpp

@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/std_code.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 #include "local_may_alias.h"