Properly handle void*

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"

src/ansi-c/Makefile

@@ -24,7 +24,6 @@ SRC = anonymous_member.cpp \
       c_typecheck_initializer.cpp \
       c_typecheck_type.cpp \
       c_typecheck_typecast.cpp \
-      c_types.cpp \
       cprover_library.cpp \
       designator.cpp \
       expr2c.cpp \

src/ansi-c/ansi_c_convert_type.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
+#include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/simplify_expr.h>
 #include <util/config.h>

src/ansi-c/ansi_c_convert_type.h

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/message.h>
 
-#include "c_types.h"
 #include "c_qualifiers.h"
 #include "c_storage_spec.h"
 

src/ansi-c/ansi_c_entry_point.cpp

@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <ansi-c/string_constant.h>
 
 #include <goto-programs/goto_functions.h>

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -10,6 +10,7 @@ Author: DiffBlue Limited. All rights reserved.
 #include <sstream>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/std_types.h>
 #include <util/std_code.h>
@@ -20,7 +21,6 @@ Author: DiffBlue Limited. All rights reserved.
 
 #include <linking/zero_initializer.h>
 
-#include <ansi-c/c_types.h>
 #include <ansi-c/string_constant.h>
 
 #include <goto-programs/goto_functions.h>

src/ansi-c/c_preprocess.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <fstream>
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/message.h>
 #include <util/tempfile.h>
@@ -29,7 +30,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/prefix.h>
 
-#include "c_types.h"
 #include "c_preprocess.h"
 
 #define GCC_DEFINES_16 \

src/ansi-c/c_sizeof.cpp

@@ -6,14 +6,14 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
 #include "c_sizeof.h"
 #include "c_typecast.h"
-#include "c_types.h"
 
 /*******************************************************************\
 

src/ansi-c/c_typecast.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/std_expr.h>
@@ -19,7 +20,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 
 #include "c_typecast.h"
-#include "c_types.h"
 #include "c_qualifiers.h"
 
 /*******************************************************************\

src/ansi-c/c_typecheck_expr.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/std_types.h>
 #include <util/prefix.h>
@@ -19,7 +20,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
-#include "c_types.h"
 #include "c_typecast.h"
 #include "c_typecheck_base.h"
 #include "c_sizeof.h"
@@ -1318,8 +1318,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
     // an integer/float of the same size
     if((expr_type.id()==ID_signedbv ||
         expr_type.id()==ID_unsignedbv) &&
-       pointer_offset_size(expr_type, *this)==
-       pointer_offset_size(op_vector_type, *this))
+       pointer_offset_bits(expr_type, *this)==
+       pointer_offset_bits(op_vector_type, *this))
     {
     }
     else

src/ansi-c/c_typecheck_initializer.cpp

@@ -7,6 +7,7 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/type_eq.h>
 #include <util/std_types.h>
@@ -16,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <linking/zero_initializer.h>
 
-#include "c_types.h"
 #include "c_typecheck_base.h"
 #include "string_constant.h"
 #include "anonymous_member.h"

src/ansi-c/c_typecheck_type.cpp

@@ -8,14 +8,14 @@ Author: Daniel Kroening, [email protected]
 
 #include <unordered_set>
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/simplify_expr.h>
 #include <util/arith_tools.h>
 #include <util/std_types.h>
 #include <util/pointer_offset_size.h>
 
 #include "c_typecheck_base.h"
-#include "c_types.h"
 #include "c_sizeof.h"
 #include "c_qualifiers.h"
 #include "ansi_c_declaration.h"

src/ansi-c/c_typecheck_typecast.cpp

@@ -8,7 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_typecast.h"
 #include "c_typecheck_base.h"
-#include "c_types.h"
 
 /*******************************************************************\
 

src/ansi-c/expr2c.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <set>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/std_types.h>
 #include <util/std_code.h>
@@ -37,7 +38,6 @@ Author: Daniel Kroening, [email protected]
 #include "c_misc.h"
 #include "c_qualifiers.h"
 #include "expr2c.h"
-#include "c_types.h"
 #include "expr2c_class.h"
 
 /*

src/ansi-c/literals/convert_character_literal.cpp

@@ -9,10 +9,9 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/std_expr.h>
 
-#include "../c_types.h"
-
 #include "unescape_string.h"
 #include "convert_character_literal.h"
 

src/ansi-c/literals/convert_float_literal.cpp

@@ -9,13 +9,13 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/ieee_float.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string2int.h>
 
-#include "../c_types.h"
 #include "parse_float.h"
 #include "convert_float_literal.h"
 

src/ansi-c/literals/convert_string_literal.cpp

@@ -9,10 +9,10 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/unicode.h>
 
 #include "../string_constant.h"
-#include "../c_types.h"
 
 #include "unescape_string.h"
 #include "convert_string_literal.h"

src/ansi-c/padding.cpp

@@ -339,6 +339,9 @@ void add_padding(union_typet &type, const namespacet &ns)
   mp_integer max_alignment=alignment(type, ns)*8;
   mp_integer size_bits=pointer_offset_bits(type, ns);
 
+  if(size_bits<0)
+    throw "type of unknown size:\n"+type.pretty();
+
   union_typet::componentst &components=type.components();
 
   // Is the union packed?

src/ansi-c/parser_static.inc

@@ -1,10 +1,9 @@
+#include <util/c_types.h>
 #include <util/std_code.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
 
-#include "c_types.h"
-
 #define YYSTYPE unsigned
 #define YYSTYPE_IS_TRIVIAL 1
 

src/ansi-c/printf_formatter.cpp

@@ -9,10 +9,10 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <sstream>
 
+#include <util/c_types.h>
 #include <util/format_constant.h>
 #include <util/simplify_expr.h>
 
-#include "c_types.h"
 #include "printf_formatter.h"
 
 /*******************************************************************\

src/ansi-c/scanner.l

@@ -21,7 +21,6 @@ static int isatty(int) { return 0; }
 
 #include <util/unicode.h>
 
-#include "c_types.h"
 #include "preprocessor_line.h"
 #include "string_constant.h"
 

src/ansi-c/string_constant.cpp

@@ -7,10 +7,10 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/std_expr.h>
 
 #include "string_constant.h"
-#include "c_types.h"
 
 /*******************************************************************\
 

src/cpp/cpp_constructor.cpp

@@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/std_types.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 
 #include "cpp_typecheck.h"
 #include "cpp_util.h"

src/cpp/cpp_convert_type.cpp

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/std_types.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 
 #include "cpp_convert_type.h"
 #include "cpp_declaration.h"

src/cpp/cpp_declarator_converter.cpp

@@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/source_location.h>
 #include <util/std_types.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 
 #include "cpp_type2name.h"
 #include "cpp_declarator_converter.h"