Make c_types widely available and avoid locally building types

Various places directly used pointer_width to build a signed/unsigned bvt.

Author: tautschnig

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

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

src/cpp/cpp_destructor.cpp

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

src/cpp/cpp_enum_type.cpp

@@ -6,7 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 
 #include "cpp_enum_type.h"
 

src/cpp/cpp_instantiate_template.cpp

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

src/cpp/cpp_typecheck_constructor.cpp

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

src/cpp/cpp_typecheck_conversions.cpp

@@ -15,7 +15,7 @@ Module: C++ Language Type Checking
 #include <util/simplify_expr.h>
 
 #include <ansi-c/c_qualifiers.h>
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 
 #include "cpp_typecheck.h"
 

src/cpp/cpp_typecheck_enum_type.cpp

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

src/cpp/cpp_typecheck_expr.cpp

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/base_type.h>
 
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <ansi-c/c_qualifiers.h>
 #include <ansi-c/c_sizeof.h>
 

src/cpp/cpp_typecheck_initializer.cpp

@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 
 #include <linking/zero_initializer.h>
-#include <ansi-c/c_types.h>
+#include <util/c_types.h>
 #include <ansi-c/c_sizeof.h>
 
 #include "cpp_typecheck.h"