From 20de0d7fa877937f3b9936bc72addd27963e5463 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 7 Apr 2017 13:33:15 +0100 Subject: [PATCH 1/2] Make c_types widely available and avoid locally building types Various places directly used pointer_width to build a signed/unsigned bvt. --- src/analyses/goto_check.cpp | 3 ++- src/analyses/invariant_set.cpp | 2 +- src/analyses/local_bitvector_analysis.cpp | 2 +- src/analyses/local_cfg.cpp | 2 +- src/analyses/local_may_alias.cpp | 2 +- src/ansi-c/Makefile | 1 - src/ansi-c/ansi_c_convert_type.cpp | 1 + src/ansi-c/ansi_c_convert_type.h | 1 - src/ansi-c/ansi_c_entry_point.cpp | 2 +- src/ansi-c/c_nondet_symbol_factory.cpp | 2 +- src/ansi-c/c_preprocess.cpp | 2 +- src/ansi-c/c_sizeof.cpp | 2 +- src/ansi-c/c_typecast.cpp | 2 +- src/ansi-c/c_typecheck_expr.cpp | 2 +- src/ansi-c/c_typecheck_initializer.cpp | 2 +- src/ansi-c/c_typecheck_type.cpp | 2 +- src/ansi-c/c_typecheck_typecast.cpp | 1 - src/ansi-c/expr2c.cpp | 2 +- .../literals/convert_character_literal.cpp | 3 +-- src/ansi-c/literals/convert_float_literal.cpp | 2 +- .../literals/convert_string_literal.cpp | 2 +- src/ansi-c/parser_static.inc | 3 +-- src/ansi-c/printf_formatter.cpp | 2 +- src/ansi-c/scanner.l | 1 - src/ansi-c/string_constant.cpp | 2 +- src/cpp/cpp_constructor.cpp | 2 +- src/cpp/cpp_convert_type.cpp | 2 +- src/cpp/cpp_declarator_converter.cpp | 2 +- src/cpp/cpp_destructor.cpp | 2 +- src/cpp/cpp_enum_type.cpp | 2 +- src/cpp/cpp_instantiate_template.cpp | 2 +- src/cpp/cpp_typecheck_constructor.cpp | 2 +- src/cpp/cpp_typecheck_conversions.cpp | 2 +- src/cpp/cpp_typecheck_enum_type.cpp | 2 +- src/cpp/cpp_typecheck_expr.cpp | 2 +- src/cpp/cpp_typecheck_initializer.cpp | 2 +- src/cpp/cpp_typecheck_resolve.cpp | 2 +- .../accelerate/polynomial_accelerator.cpp | 3 ++- src/goto-instrument/function.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 7 +++--- src/goto-programs/builtin_functions.cpp | 2 +- src/goto-programs/format_strings.cpp | 2 +- src/goto-programs/goto_clean_expr.cpp | 2 +- src/goto-programs/goto_convert.cpp | 2 +- .../goto_convert_function_call.cpp | 2 +- .../goto_convert_new_switch_case.cpp | 2 +- .../goto_convert_side_effect.cpp | 2 +- src/goto-programs/graphml_witness.cpp | 3 ++- .../remove_function_pointers.cpp | 2 +- src/goto-programs/string_abstraction.cpp | 2 +- src/goto-programs/string_instrumentation.cpp | 2 +- src/goto-symex/rewrite_union.cpp | 2 +- src/goto-symex/symex_assign.cpp | 2 +- src/goto-symex/symex_builtin_functions.cpp | 2 +- src/goto-symex/symex_clean_expr.cpp | 2 +- src/goto-symex/symex_dereference.cpp | 2 +- src/goto-symex/symex_function_call.cpp | 2 +- src/goto-symex/symex_other.cpp | 2 +- .../java_bytecode_internal_additions.cpp | 2 +- src/java_bytecode/java_entry_point.cpp | 2 +- src/jsil/jsil_internal_additions.cpp | 2 +- src/linking/static_lifetime_init.cpp | 2 +- src/linking/zero_initializer.cpp | 2 +- src/path-symex/path_symex.cpp | 2 +- src/path-symex/path_symex_state.cpp | 2 +- src/pointer-analysis/dereference.cpp | 2 +- src/pointer-analysis/value_set.cpp | 2 +- .../value_set_dereference.cpp | 2 +- src/pointer-analysis/value_set_fi.cpp | 2 +- src/pointer-analysis/value_set_fivr.cpp | 2 +- src/pointer-analysis/value_set_fivrns.cpp | 2 +- src/solvers/flattening/boolbv_update.cpp | 2 +- src/solvers/qbf/qbf_squolem_core.cpp | 2 +- src/util/Makefile | 1 + src/{ansi-c => util}/c_types.cpp | 4 ++-- src/{ansi-c => util}/c_types.h | 8 +++---- src/util/pointer_offset_size.cpp | 24 +++++++++---------- src/util/pointer_predicates.cpp | 19 +++++++++------ src/util/simplify_expr.cpp | 13 +++++----- src/util/simplify_expr_pointer.cpp | 7 +++--- src/util/std_expr.cpp | 13 +++++----- 81 files changed, 120 insertions(+), 120 deletions(-) rename src/{ansi-c => util}/c_types.cpp (99%) rename src/{ansi-c => util}/c_types.h (89%) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index cc418d6aed9..10749025515 100644 --- a/src/analyses/goto_check.cpp +++ b/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); diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index 19531e96092..3dae9eb1312 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include "invariant_set.h" diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 777cf4aacc2..308b8b79e65 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include "local_bitvector_analysis.h" diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp index 52f5c6831a4..0990331e586 100644 --- a/src/analyses/local_cfg.cpp +++ b/src/analyses/local_cfg.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #endif diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index ffaefe73667..c59b89b534c 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include "local_may_alias.h" diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index cfee8e68f07..d98dce4e3c1 100644 --- a/src/ansi-c/Makefile +++ b/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 \ diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 7dc6f2165cf..d4777888b7e 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index 0fef20b4928..4239d1715b1 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "c_types.h" #include "c_qualifiers.h" #include "c_storage_spec.h" diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index ecb2dcc73cd..070bf4ad2dd 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 9149d6f8786..ae7f7c63875 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -10,6 +10,7 @@ Author: DiffBlue Limited. All rights reserved. #include #include +#include #include #include #include @@ -20,7 +21,6 @@ Author: DiffBlue Limited. All rights reserved. #include -#include #include #include diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index 9582d6f3b00..490d2399eaa 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -29,7 +30,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "c_types.h" #include "c_preprocess.h" #define GCC_DEFINES_16 \ diff --git a/src/ansi-c/c_sizeof.cpp b/src/ansi-c/c_sizeof.cpp index 85c91870208..c247ac9d402 100644 --- a/src/ansi-c/c_sizeof.cpp +++ b/src/ansi-c/c_sizeof.cpp @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include #include @@ -13,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_sizeof.h" #include "c_typecast.h" -#include "c_types.h" /*******************************************************************\ diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 52070e29257..a20a190854a 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -19,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "c_typecast.h" -#include "c_types.h" #include "c_qualifiers.h" /*******************************************************************\ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 5d4788e5145..534bfacd994 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -19,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "c_types.h" #include "c_typecast.h" #include "c_typecheck_base.h" #include "c_sizeof.h" diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 79dabc9f0e9..5855887e297 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include #include #include #include @@ -16,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "c_types.h" #include "c_typecheck_base.h" #include "string_constant.h" #include "anonymous_member.h" diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index ac3fe7f2928..805293f7f0f 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -15,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "c_typecheck_base.h" -#include "c_types.h" #include "c_sizeof.h" #include "c_qualifiers.h" #include "ansi_c_declaration.h" diff --git a/src/ansi-c/c_typecheck_typecast.cpp b/src/ansi-c/c_typecheck_typecast.cpp index 5d1cfad1332..f76c3eb7556 100644 --- a/src/ansi-c/c_typecheck_typecast.cpp +++ b/src/ansi-c/c_typecheck_typecast.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_typecast.h" #include "c_typecheck_base.h" -#include "c_types.h" /*******************************************************************\ diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index cc631e12da2..379f7b6288f 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -37,7 +38,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_misc.h" #include "c_qualifiers.h" #include "expr2c.h" -#include "c_types.h" #include "expr2c_class.h" /* diff --git a/src/ansi-c/literals/convert_character_literal.cpp b/src/ansi-c/literals/convert_character_literal.cpp index f76af2eefa6..abd4a22b322 100644 --- a/src/ansi-c/literals/convert_character_literal.cpp +++ b/src/ansi-c/literals/convert_character_literal.cpp @@ -9,10 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include "../c_types.h" - #include "unescape_string.h" #include "convert_character_literal.h" diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp index 7e72f6e6f53..0f1ab0a5f36 100644 --- a/src/ansi-c/literals/convert_float_literal.cpp +++ b/src/ansi-c/literals/convert_float_literal.cpp @@ -9,13 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include #include #include -#include "../c_types.h" #include "parse_float.h" #include "convert_float_literal.h" diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp index 4176581afe2..ebf166b222b 100644 --- a/src/ansi-c/literals/convert_string_literal.cpp +++ b/src/ansi-c/literals/convert_string_literal.cpp @@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include "../string_constant.h" -#include "../c_types.h" #include "unescape_string.h" #include "convert_string_literal.h" diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc index 13ac3e18973..e0c8385998d 100644 --- a/src/ansi-c/parser_static.inc +++ b/src/ansi-c/parser_static.inc @@ -1,10 +1,9 @@ +#include #include #include #include #include -#include "c_types.h" - #define YYSTYPE unsigned #define YYSTYPE_IS_TRIVIAL 1 diff --git a/src/ansi-c/printf_formatter.cpp b/src/ansi-c/printf_formatter.cpp index 31ddfa735f2..46e831a9853 100644 --- a/src/ansi-c/printf_formatter.cpp +++ b/src/ansi-c/printf_formatter.cpp @@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include -#include "c_types.h" #include "printf_formatter.h" /*******************************************************************\ diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 2b58bd40c9f..7a97b0a7b89 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -21,7 +21,6 @@ static int isatty(int) { return 0; } #include -#include "c_types.h" #include "preprocessor_line.h" #include "string_constant.h" diff --git a/src/ansi-c/string_constant.cpp b/src/ansi-c/string_constant.cpp index 6576a99ea5b..c0791c10f25 100644 --- a/src/ansi-c/string_constant.cpp +++ b/src/ansi-c/string_constant.cpp @@ -7,10 +7,10 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include #include #include "string_constant.h" -#include "c_types.h" /*******************************************************************\ diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index 3c5b34762dd..a8f12b52869 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include "cpp_typecheck.h" #include "cpp_util.h" diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index 208fa821ad9..07899e63ce9 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include "cpp_convert_type.h" #include "cpp_declaration.h" diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 24a295a03f7..1eb9b07b43a 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include "cpp_type2name.h" #include "cpp_declarator_converter.h" diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index 75479a0ee85..44833ce84c5 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include +#include #include "cpp_typecheck.h" diff --git a/src/cpp/cpp_enum_type.cpp b/src/cpp/cpp_enum_type.cpp index ba4bc6ecbae..a1f552f4119 100644 --- a/src/cpp/cpp_enum_type.cpp +++ b/src/cpp/cpp_enum_type.cpp @@ -6,7 +6,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include +#include #include "cpp_enum_type.h" diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index 34b1d358cb0..ca4b8f113f5 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include "cpp_type2name.h" #include "cpp_typecheck.h" diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index 24b45dda74b..78e92dcc74c 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include "cpp_typecheck.h" #include "cpp_util.h" diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index a38629bdf41..9db89b0d625 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -15,7 +15,7 @@ Module: C++ Language Type Checking #include #include -#include +#include #include "cpp_typecheck.h" diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index 09c57e9e9bc..1022b48b718 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "cpp_typecheck.h" #include "cpp_enum_type.h" diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 45569d8d9f3..633915d6609 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include #include diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index f51490e77f8..b6a7fb5a998 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include #include "cpp_typecheck.h" diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 488e912dc42..0c3916b5d31 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include #include diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index 5f712b55f5e..87bc392711f 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -22,6 +22,7 @@ Author: Matt Lewis #include +#include #include #include #include @@ -516,7 +517,7 @@ void polynomial_acceleratort::assert_for_values( #ifdef DEBUG std::cout << "Overriding pointer type\n"; #endif - this_type=unsignedbv_typet(config.ansi_c.pointer_width); + this_type=size_type(); } if(expr_type==nil_typet()) diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index 1ad749814bd..6e59fc9d051 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include "function.h" diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 400aca3b407..7432bb67c5e 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -479,9 +480,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs( static_cast(r.find(ID_C_va_arg_type)); dereference_exprt deref( - typecast_exprt( - from_integer(0, signedbv_typet(config.ansi_c.pointer_width)), - pointer_typet(va_arg_type)), + null_pointer_exprt(pointer_typet(va_arg_type)), va_arg_type); type_of.arguments().push_back(deref); @@ -530,7 +529,7 @@ void goto_program2codet::convert_assign_rec( { index_exprt index( assign.lhs(), - from_integer(i++, signedbv_typet(config.ansi_c.pointer_width)), + from_integer(i++, index_type()), type.subtype()); convert_assign_rec(code_assignt(index, *it), dest); } diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index d6f1be13a71..078e56f7e0d 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -24,7 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include #include "goto_convert_class.h" diff --git a/src/goto-programs/format_strings.cpp b/src/goto-programs/format_strings.cpp index 1e8be3b09cd..40f2be4a116 100644 --- a/src/goto-programs/format_strings.cpp +++ b/src/goto-programs/format_strings.cpp @@ -9,7 +9,7 @@ Author: CM Wintersteiger #include #include -#include +#include #include diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index c7fa8637194..dbfbaaa01c8 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_convert_class.h" diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 25118d0b223..cbc3fc420b4 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_convert.h" #include "goto_convert_class.h" diff --git a/src/goto-programs/goto_convert_function_call.cpp b/src/goto-programs/goto_convert_function_call.cpp index 6fe2b42bbc1..d3ca9abb493 100644 --- a/src/goto-programs/goto_convert_function_call.cpp +++ b/src/goto-programs/goto_convert_function_call.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_convert_class.h" diff --git a/src/goto-programs/goto_convert_new_switch_case.cpp b/src/goto-programs/goto_convert_new_switch_case.cpp index 4a81a4176a2..ba46d2f0ec6 100644 --- a/src/goto-programs/goto_convert_new_switch_case.cpp +++ b/src/goto-programs/goto_convert_new_switch_case.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_convert.h" #include "goto_convert_class.h" diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index dbebb856ec1..2a1516ff090 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_convert_class.h" diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index ae10705e232..43bd009190b 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening #include #include +#include #include #include #include @@ -81,7 +82,7 @@ std::string graphml_witnesst::convert_assign_rec( { index_exprt index( assign.lhs(), - from_integer(i++, signedbv_typet(config.ansi_c.pointer_width)), + from_integer(i++, index_type()), type.subtype()); if(!result.empty()) result+=' '; diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 2d5be9c0ab2..d1ede2833db 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "remove_skip.h" #include "remove_function_pointers.h" diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 5c7a1868578..1e47574d436 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "pointer_arithmetic.h" #include "string_abstraction.h" diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 5a6596a97cd..2bfefa81d11 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "string_instrumentation.h" diff --git a/src/goto-symex/rewrite_union.cpp b/src/goto-symex/rewrite_union.cpp index f0a329af5ae..e21784c7fbb 100644 --- a/src/goto-symex/rewrite_union.cpp +++ b/src/goto-symex/rewrite_union.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include "rewrite_union.h" diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 61b6ad28488..796efc3e769 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_symex.h" #include "goto_symex_state.h" diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index c5bdd32d0f2..6cfd60073ad 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index e3e650d7b99..684fd6b0123 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_symex.h" diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 4d3ca06e358..c001ad792fe 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_symex.h" #include "symex_dereference_state.h" diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 00636ae339b..83b2da4bcd8 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 315447093ea..56d5d40c832 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_symex.h" diff --git a/src/java_bytecode/java_bytecode_internal_additions.cpp b/src/java_bytecode/java_bytecode_internal_additions.cpp index c0d019a4cc4..2432f112fdf 100644 --- a/src/java_bytecode/java_bytecode_internal_additions.cpp +++ b/src/java_bytecode/java_bytecode_internal_additions.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "java_bytecode_internal_additions.h" diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 7eb348986a5..d2f14e93cf6 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include diff --git a/src/jsil/jsil_internal_additions.cpp b/src/jsil/jsil_internal_additions.cpp index 9f583fbb56b..be2947edd51 100644 --- a/src/jsil/jsil_internal_additions.cpp +++ b/src/jsil/jsil_internal_additions.cpp @@ -10,7 +10,7 @@ Author: Michael Tautschnig, tautschn@amazon.com #include #include -#include +#include #include "jsil_types.h" diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 29f5005d685..507df13bac3 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include diff --git a/src/linking/zero_initializer.cpp b/src/linking/zero_initializer.cpp index 9e96c48480b..e88becbb6a8 100644 --- a/src/linking/zero_initializer.cpp +++ b/src/linking/zero_initializer.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include "zero_initializer.h" diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index 757407ba79b..1fc32589b6d 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include +#include #include diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp index 87843da304d..34eb7d49367 100644 --- a/src/path-symex/path_symex_state.cpp +++ b/src/path-symex/path_symex_state.cpp @@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp index 51a4993bd19..8509f8743d5 100644 --- a/src/pointer-analysis/dereference.cpp +++ b/src/pointer-analysis/dereference.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "dereference.h" diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 799921bbf75..e9853dd7d25 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #ifdef DEBUG #include diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index a5738b363b2..cfcaad757b5 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index f7895d3aaf1..89975646131 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "value_set_fi.h" diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index a780648446b..c91c19430b7 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com, #include #include -#include +#include #include "value_set_fivr.h" diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 5e5836de25c..2d77c78876f 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com, #include #include -#include +#include #include "value_set_fivrns.h" diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp index 2b485781f6b..2bbeacca47d 100644 --- a/src/solvers/flattening/boolbv_update.cpp +++ b/src/solvers/flattening/boolbv_update.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "boolbv.h" diff --git a/src/solvers/qbf/qbf_squolem_core.cpp b/src/solvers/qbf/qbf_squolem_core.cpp index 547644c7d29..cdbdc568d4f 100644 --- a/src/solvers/qbf/qbf_squolem_core.cpp +++ b/src/solvers/qbf/qbf_squolem_core.cpp @@ -11,7 +11,7 @@ Author: CM Wintersteiger #include #include -#include // uint type for indices +#include // uint type for indices #include "qbf_squolem_core.h" diff --git a/src/util/Makefile b/src/util/Makefile index 154792d1331..ce4489b18ce 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -3,6 +3,7 @@ SRC = arith_tools.cpp \ base_type.cpp \ bv_arithmetic.cpp \ byte_operators.cpp \ + c_types.cpp \ cmdline.cpp \ config.cpp \ cout_message.cpp \ diff --git a/src/ansi-c/c_types.cpp b/src/util/c_types.cpp similarity index 99% rename from src/ansi-c/c_types.cpp rename to src/util/c_types.cpp index 6ba5ddaefb3..dbb2450f40a 100644 --- a/src/ansi-c/c_types.cpp +++ b/src/util/c_types.cpp @@ -6,8 +6,8 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include -#include +#include "std_types.h" +#include "config.h" #include "c_types.h" diff --git a/src/ansi-c/c_types.h b/src/util/c_types.h similarity index 89% rename from src/ansi-c/c_types.h rename to src/util/c_types.h index 6c571bd448b..2735f594f7f 100644 --- a/src/ansi-c/c_types.h +++ b/src/util/c_types.h @@ -6,10 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#ifndef CPROVER_ANSI_C_C_TYPES_H -#define CPROVER_ANSI_C_C_TYPES_H +#ifndef CPROVER_UTIL_C_TYPES_H +#define CPROVER_UTIL_C_TYPES_H -#include +#include "type.h" typet index_type(); typet enum_constant_type(); @@ -44,4 +44,4 @@ typet void_type(); // ID_signed_int gets "signed int". std::string c_type_as_string(const irep_idt &); -#endif // CPROVER_ANSI_C_C_TYPES_H +#endif // CPROVER_UTIL_C_TYPES_H diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 43e7dd0d5a9..de7d5041230 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "c_types.h" #include "expr.h" #include "arith_tools.h" #include "std_types.h" @@ -273,7 +274,7 @@ exprt member_offset_expr( return member_offset_expr( to_struct_type(type), member_expr.get_component_name(), ns); else if(type.id()==ID_union) - return from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(0, signed_size_type()); else return nil_exprt(); } @@ -297,7 +298,7 @@ exprt member_offset_expr( { const struct_typet::componentst &components=type.components(); - exprt result=from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); + exprt result=from_integer(0, signed_size_type()); std::size_t bit_field_bits=0; for(struct_typet::componentst::const_iterator @@ -407,7 +408,7 @@ exprt size_of_expr( const struct_typet::componentst &components= struct_type.components(); - exprt result=from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); + exprt result=from_integer(0, size_type()); std::size_t bit_field_bits=0; for(struct_typet::componentst::const_iterator @@ -470,7 +471,7 @@ exprt size_of_expr( result=sub_size; } - return from_integer(result, signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(result, size_type()); } else if(type.id()==ID_signedbv || type.id()==ID_unsignedbv || @@ -483,7 +484,7 @@ exprt size_of_expr( std::size_t bytes=width/8; if(bytes*8!=width) bytes++; - return from_integer(bytes, signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(bytes, size_type()); } else if(type.id()==ID_c_enum) { @@ -491,7 +492,7 @@ exprt size_of_expr( std::size_t bytes=width/8; if(bytes*8!=width) bytes++; - return from_integer(bytes, signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(bytes, size_type()); } else if(type.id()==ID_c_enum_tag) { @@ -499,7 +500,7 @@ exprt size_of_expr( } else if(type.id()==ID_bool) { - return from_integer(1, signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(1, size_type()); } else if(type.id()==ID_pointer) { @@ -507,7 +508,7 @@ exprt size_of_expr( std::size_t bytes=width/8; if(bytes*8!=width) bytes++; - return from_integer(bytes, signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(bytes, size_type()); } else if(type.id()==ID_symbol) { @@ -515,12 +516,11 @@ exprt size_of_expr( } else if(type.id()==ID_code) { - return from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(0, size_type()); } else if(type.id()==ID_string) { - return from_integer( - 32/8, signedbv_typet(config.ansi_c.pointer_width)); + return from_integer(32/8, size_type()); } else return nil_exprt(); @@ -628,7 +628,7 @@ exprt build_sizeof_expr( return nil_exprt(); assert(address_bits(val+1)<=config.ansi_c.pointer_width); - const unsignedbv_typet t(config.ansi_c.pointer_width); + const typet t(size_type()); mp_integer remainder=0; if(type_size!=0) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 53427d056e2..ed027cce536 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include "c_types.h" #include "cprover_prefix.h" #include "namespace.h" #include "std_expr.h" @@ -31,9 +32,7 @@ Function: pointer_object exprt pointer_object(const exprt &p) { - return unary_exprt( - ID_pointer_object, p, - unsignedbv_typet(config.ansi_c.pointer_width)); + return unary_exprt(ID_pointer_object, p, size_type()); } /*******************************************************************\ @@ -67,8 +66,7 @@ Function: object_size exprt object_size(const exprt &pointer) { - typet type=signedbv_typet(config.ansi_c.pointer_width); - return unary_exprt(ID_object_size, pointer, type); + return unary_exprt(ID_object_size, pointer, size_type()); } /*******************************************************************\ @@ -85,8 +83,7 @@ Function: pointer_offset exprt pointer_offset(const exprt &pointer) { - typet type=signedbv_typet(config.ansi_c.pointer_width); - return unary_exprt(ID_pointer_offset, pointer, type); + return unary_exprt(ID_pointer_offset, pointer, signed_size_type()); } /*******************************************************************\ @@ -411,6 +408,10 @@ exprt dynamic_object_upper_bound( if(access_size.is_not_nil()) { op=ID_gt; + + if(ns.follow(object_offset.type())!= + ns.follow(access_size.type())) + object_offset.make_typecast(access_size.type()); sum=plus_exprt(object_offset, access_size); } @@ -453,6 +454,10 @@ exprt object_upper_bound( if(access_size.is_not_nil()) { op=ID_gt; + + if(ns.follow(object_offset.type())!= + ns.follow(access_size.type())) + object_offset.make_typecast(access_size.type()); sum=plus_exprt(object_offset, access_size); } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 837138258d0..535f8d92048 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "c_types.h" #include "rational.h" #include "simplify_expr_class.h" #include "simplify_expr.h" @@ -334,7 +335,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) expr.op0().operands().size()==1 && op_type.id()==ID_pointer) { - expr.op0().type()=unsignedbv_typet(config.ansi_c.pointer_width); + expr.op0().type()=size_type(); simplify_typecast(expr.op0()); // rec. call simplify_typecast(expr); // rec. call return false; @@ -351,17 +352,15 @@ bool simplify_exprt::simplify_typecast(exprt &expr) expr.op0().op0().op0().is_zero() && op_type.id()==ID_pointer) { - unsignedbv_typet size_type(config.ansi_c.pointer_width); - mp_integer sub_size=pointer_offset_size(op_type.subtype(), ns); if(sub_size!=-1) { // void* if(sub_size==0 || sub_size==1) - expr.op0()=typecast_exprt(expr.op0().op1(), size_type); + expr.op0()=typecast_exprt(expr.op0().op1(), size_type()); else - expr.op0()=mult_exprt(from_integer(sub_size, size_type), - typecast_exprt(expr.op0().op1(), size_type)); + expr.op0()=mult_exprt(from_integer(sub_size, size_type()), + typecast_exprt(expr.op0().op1(), size_type())); simplify_rec(expr.op0()); simplify_typecast(expr); // rec. call @@ -428,7 +427,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) if(step>0) { - const unsignedbv_typet size_t_type(config.ansi_c.pointer_width); + const typet size_t_type(size_type()); expr.op0().type()=size_t_type; for(auto &op : expr.op0().operands()) diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 9bc2496f5ff..b1d070b85c9 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "c_types.h" #include "simplify_expr_class.h" #include "expr.h" #include "namespace.h" @@ -100,11 +101,10 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr) if(!to_integer(expr.op1(), index) && step_size!=-1) { - unsignedbv_typet int_type(config.ansi_c.pointer_width); pointer_typet pointer_type; pointer_type.subtype()=expr.type(); typecast_exprt typecast_expr( - from_integer(step_size*index+address, int_type), pointer_type); + from_integer(step_size*index+address, index_type()), pointer_type); exprt new_expr=dereference_exprt(typecast_expr, expr.type()); expr=new_expr; result=true; @@ -137,11 +137,10 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr) mp_integer offset=member_offset(struct_type, member, ns); if(offset!=-1) { - unsignedbv_typet int_type(config.ansi_c.pointer_width); pointer_typet pointer_type; pointer_type.subtype()=expr.type(); typecast_exprt typecast_expr( - from_integer(address+offset, int_type), pointer_type); + from_integer(address+offset, index_type()), pointer_type); exprt new_expr=dereference_exprt(typecast_expr, expr.type()); expr=new_expr; result=true; diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 4cb9eeff9cc..d298d80e3dd 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "byte_operators.h" +#include "c_types.h" #include "config.h" #include "namespace.h" #include "pointer_offset_size.h" @@ -114,8 +115,6 @@ static void build_object_descriptor_rec( const exprt &expr, object_descriptor_exprt &dest) { - const signedbv_typet index_type(config.ansi_c.pointer_width); - if(expr.id()==ID_index) { const index_exprt &index=to_index_expr(expr); @@ -127,8 +126,8 @@ static void build_object_descriptor_rec( dest.offset()= plus_exprt(dest.offset(), - mult_exprt(typecast_exprt(index.index(), index_type), - typecast_exprt(sub_size, index_type))); + mult_exprt(typecast_exprt(index.index(), index_type()), + typecast_exprt(sub_size, index_type()))); } else if(expr.id()==ID_member) { @@ -142,7 +141,7 @@ static void build_object_descriptor_rec( dest.offset()= plus_exprt(dest.offset(), - typecast_exprt(offset, index_type)); + typecast_exprt(offset, index_type())); } else if(expr.id()==ID_byte_extract_little_endian || expr.id()==ID_byte_extract_big_endian) @@ -156,7 +155,7 @@ static void build_object_descriptor_rec( dest.offset()= plus_exprt(dest.offset(), typecast_exprt(to_byte_extract_expr(expr).offset(), - index_type)); + index_type())); } else if(expr.id()==ID_typecast) { @@ -188,7 +187,7 @@ void object_descriptor_exprt::build( object()=expr; if(offset().id()==ID_unknown) - offset()=from_integer(0, signedbv_typet(config.ansi_c.pointer_width)); + offset()=from_integer(0, index_type()); build_object_descriptor_rec(ns, expr, *this); From 7f6443b1b0a584c9dda152553faec53e39222013 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 May 2017 09:08:34 +0100 Subject: [PATCH 2/2] The sub-size of void* is undefined; use char* as specified in the standard This patch includes a review of all uses of functions from pointer_offset_size.h as all of those may return nil or a negative number if the size could not be determined. Calling sites need to handle those cases as appropriate in a given context. --- regression/cbmc/void_pointer1/main.c | 12 ++++++++ regression/cbmc/void_pointer1/test.desc | 8 ++++++ regression/cbmc/void_pointer2/main.c | 12 ++++++++ regression/cbmc/void_pointer2/test.desc | 8 ++++++ src/analyses/goto_rw.cpp | 1 + src/ansi-c/c_typecheck_expr.cpp | 4 +-- src/ansi-c/padding.cpp | 3 ++ src/goto-instrument/alignment_checks.cpp | 6 ++++ src/pointer-analysis/value_set.cpp | 28 ++++++++++++++++--- .../value_set_dereference.cpp | 9 ++++++ src/solvers/cvc/cvc_conv.cpp | 1 + src/solvers/dplib/dplib_conv.cpp | 1 + src/solvers/flattening/bv_pointers.cpp | 12 +++++++- .../flattening/flatten_byte_operators.cpp | 8 ++++-- src/solvers/flattening/pointer_logic.cpp | 3 +- src/solvers/smt1/smt1_conv.cpp | 2 ++ src/solvers/smt2/smt2_conv.cpp | 3 ++ src/util/pointer_offset_size.cpp | 16 ++++++++++- src/util/simplify_expr_pointer.cpp | 8 ++++-- 19 files changed, 130 insertions(+), 15 deletions(-) create mode 100644 regression/cbmc/void_pointer1/main.c create mode 100644 regression/cbmc/void_pointer1/test.desc create mode 100644 regression/cbmc/void_pointer2/main.c create mode 100644 regression/cbmc/void_pointer2/test.desc diff --git a/regression/cbmc/void_pointer1/main.c b/regression/cbmc/void_pointer1/main.c new file mode 100644 index 00000000000..db79440d471 --- /dev/null +++ b/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); +} diff --git a/regression/cbmc/void_pointer1/test.desc b/regression/cbmc/void_pointer1/test.desc new file mode 100644 index 00000000000..39c491ba8bb --- /dev/null +++ b/regression/cbmc/void_pointer1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/void_pointer2/main.c b/regression/cbmc/void_pointer2/main.c new file mode 100644 index 00000000000..db79440d471 --- /dev/null +++ b/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); +} diff --git a/regression/cbmc/void_pointer2/test.desc b/regression/cbmc/void_pointer2/test.desc new file mode 100644 index 00000000000..3556481d977 --- /dev/null +++ b/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 diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 6541ca45283..ae0255fe6f5 100644 --- a/src/analyses/goto_rw.cpp +++ b/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; diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 534bfacd994..207763608c2 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -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 diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index 16391ee33a7..602d9239710 100644 --- a/src/ansi-c/padding.cpp +++ b/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? diff --git a/src/goto-instrument/alignment_checks.cpp b/src/goto-instrument/alignment_checks.cpp index 0daa8327492..01b21703fef 100644 --- a/src/goto-instrument/alignment_checks.cpp +++ b/src/goto-instrument/alignment_checks.cpp @@ -60,6 +60,9 @@ void print_struct_alignment_problems( const namespacet ns(symbol_table); mp_integer size=pointer_offset_size(it_type, ns); + if(size<0) + throw "type of unknown size:\n"+it_type.pretty(); + cumulated_length+=size; // [it_mem;it_next] cannot be covered by an instruction if(cumulated_length>config.ansi_c.memory_operand_size) @@ -99,6 +102,9 @@ void print_struct_alignment_problems( const mp_integer size= pointer_offset_size(array.subtype(), ns); + if(size<0) + throw "type of unknown size:\n"+it_type.pretty(); + if(2*integer2long(size)<=config.ansi_c.memory_operand_size) { out << "\nWARNING: " diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index e9853dd7d25..96b6acbe204 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -717,10 +717,23 @@ void value_sett::get_value_set_rec( if(i_is_set) { - i*=pointer_offset_size(ptr_operand.type().subtype(), ns); + typet pointer_sub_type=ptr_operand.type().subtype(); + if(pointer_sub_type.id()==ID_empty) + pointer_sub_type=char_type(); - if(expr.id()==ID_minus) - i.negate(); + mp_integer size=pointer_offset_size(pointer_sub_type, ns); + + if(size<=0) + { + i_is_set=false; + } + else + { + i*=size; + + if(expr.id()==ID_minus) + i.negate(); + } } get_value_set_rec( @@ -1155,7 +1168,14 @@ void value_sett::get_reference_set_rec( } else if(!to_integer(offset, i) && o.offset_is_zero()) - o.offset=i*pointer_offset_size(array_type.subtype(), ns); + { + mp_integer size=pointer_offset_size(array_type.subtype(), ns); + + if(size<=0) + o.offset_is_set=false; + else + o.offset=i*size; + } else o.offset_is_set=false; diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index cfcaad757b5..36e294d263a 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -566,6 +566,10 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // no need to adjust offset adjusted_offset=offset; } + else if(element_size<=0) + { + throw "unknown or invalid type size of:\n"+dereference_type.pretty(); + } else { exprt element_size_expr= @@ -965,7 +969,12 @@ bool value_set_dereferencet::memory_model_bytes( // upper bound { mp_integer from_width=pointer_offset_size(from_type, ns); + if(from_width<=0) + throw "unknown or invalid type size:\n"+from_type.pretty(); + mp_integer to_width=pointer_offset_size(to_type, ns); + if(to_width<=0) + throw "unknown or invalid type size:\n"+to_type.pretty(); exprt bound=from_integer(from_width-to_width, offset.type()); diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp index 2d02b12a2c5..bd1e6618601 100644 --- a/src/solvers/cvc/cvc_conv.cpp +++ b/src/solvers/cvc/cvc_conv.cpp @@ -835,6 +835,7 @@ void cvc_convt::convert_address_of_rec(const exprt &expr) to_struct_type(struct_op.type()), component_name, ns); + assert(offset>=0); typet index_type(ID_unsignedbv); index_type.set(ID_width, config.ansi_c.pointer_width); diff --git a/src/solvers/dplib/dplib_conv.cpp b/src/solvers/dplib/dplib_conv.cpp index 2ce10b9400e..27fb700f8ed 100644 --- a/src/solvers/dplib/dplib_conv.cpp +++ b/src/solvers/dplib/dplib_conv.cpp @@ -218,6 +218,7 @@ void dplib_convt::convert_address_of_rec(const exprt &expr) mp_integer offset=member_offset(ns, to_struct_type(struct_op.type()), component_name); + assert(offset>=0); typet index_type(ID_unsignedbv); index_type.set(ID_width, config.ansi_c.pointer_width); diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index e026b6c3de7..5740b24bd95 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include #include @@ -185,6 +186,7 @@ bool bv_pointerst::convert_address_of_rec( // get size mp_integer size= pointer_offset_size(array_type.subtype(), ns); + assert(size>0); offset_arithmetic(bv, size, index); assert(bv.size()==bits); @@ -205,6 +207,7 @@ bool bv_pointerst::convert_address_of_rec( mp_integer offset=member_offset( to_struct_type(struct_op_type), member_expr.get_component_name(), ns); + assert(offset>=0); // add offset offset_arithmetic(bv, offset); @@ -375,7 +378,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) count++; bv=convert_bv(*it); assert(bv.size()==bits); - size=pointer_offset_size(it->type().subtype(), ns); + + typet pointer_sub_type=it->type().subtype(); + if(pointer_sub_type.id()==ID_empty) + pointer_sub_type=char_type(); + size=pointer_offset_size(pointer_sub_type, ns); + assert(size>0); } } @@ -449,6 +457,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) mp_integer element_size= pointer_offset_size(expr.op0().type().subtype(), ns); + assert(element_size>0); offset_arithmetic(bv, element_size, neg_op1); @@ -517,6 +526,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) mp_integer element_size= pointer_offset_size(expr.op0().type().subtype(), ns); + assert(element_size>0); if(element_size!=1) { diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp index 68ad4b9197e..a9597e635af 100644 --- a/src/solvers/flattening/flatten_byte_operators.cpp +++ b/src/solvers/flattening/flatten_byte_operators.cpp @@ -197,6 +197,8 @@ exprt flatten_byte_update( mp_integer element_size= pointer_offset_size(src.op2().type(), ns); + if(element_size<0) + throw "byte_update of unknown width:\n"+src.pretty(); const typet &t=ns.follow(src.op0().type()); @@ -378,9 +380,9 @@ exprt flatten_byte_update( t.id()==ID_pointer) { // do a shift, mask and OR - std::size_t width=integer2size_t(pointer_offset_size(t, ns)*8); - - assert(width!=0); + mp_integer type_width=pointer_offset_bits(t, ns); + assert(type_width>0); + std::size_t width=integer2size_t(type_width); if(element_size*8>width) throw "flatten_byte_update to update element that is too large"; diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index c2b9d1175d0..c52a9798b1d 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -200,7 +200,7 @@ exprt pointer_logict::object_rec( mp_integer size= pointer_offset_size(src.type().subtype(), ns); - if(size==0) + if(size<=0) return src; mp_integer index=offset/size; @@ -234,6 +234,7 @@ exprt pointer_logict::object_rec( const typet &subtype=it->type(); mp_integer sub_size=pointer_offset_size(subtype, ns); + assert(sub_size>0); mp_integer new_offset=current_offset+sub_size; if(new_offset>offset) diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index e9b71d87956..94e42f67f7f 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -432,6 +432,7 @@ void smt1_convt::convert_address_of_rec( member_expr.get_component_name(); mp_integer offset=member_offset(struct_type, component_name, ns); + assert(offset>=0); typet index_type(ID_unsignedbv); index_type.set(ID_width, boolbv_width(result_type)); @@ -2333,6 +2334,7 @@ void smt1_convt::convert_plus(const plus_exprt &expr) mp_integer element_size= pointer_offset_size(expr.type().subtype(), ns); + assert(element_size>0); // adjust width if needed if(boolbv_width(i.type())!=boolbv_width(expr.type())) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 37a3647ed71..a7b07972c22 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -694,6 +694,7 @@ void smt2_convt::convert_address_of_rec( member_expr.get_component_name(); mp_integer offset=member_offset(struct_type, component_name, ns); + assert(offset>=0); unsignedbv_typet index_type; index_type.set_width(boolbv_width(result_type)); @@ -3253,6 +3254,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr) mp_integer element_size= pointer_offset_size(expr.type().subtype(), ns); + assert(element_size>0); out << "(bvadd "; convert_expr(p); @@ -3469,6 +3471,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr) // Pointer difference. mp_integer element_size= pointer_offset_size(expr.op0().type().subtype(), ns); + assert(element_size>0); if(element_size>=2) out << "(bvsdiv "; diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index de7d5041230..7ab752c898f 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -130,6 +130,8 @@ mp_integer pointer_offset_bits( if(type.id()==ID_array) { mp_integer sub=pointer_offset_bits(type.subtype(), ns); + if(sub<0) + return -1; // get size const exprt &size=to_array_type(type).size(); @@ -145,6 +147,8 @@ mp_integer pointer_offset_bits( else if(type.id()==ID_vector) { mp_integer sub=pointer_offset_bits(type.subtype(), ns); + if(sub<0) + return -1; // get size const exprt &size=to_vector_type(type).size(); @@ -160,6 +164,9 @@ mp_integer pointer_offset_bits( else if(type.id()==ID_complex) { mp_integer sub=pointer_offset_bits(type.subtype(), ns); + if(sub<0) + return -1; + return sub*2; } else if(type.id()==ID_struct) @@ -201,6 +208,8 @@ mp_integer pointer_offset_bits( { const typet &subtype=it->type(); mp_integer sub_size=pointer_offset_bits(subtype, ns); + if(sub_size==-1) + return -1; if(sub_size>result) result=sub_size; } @@ -467,6 +476,11 @@ exprt size_of_expr( else sub_size=pointer_offset_size(subtype, ns); + if(sub_size==-1) + { + result=-1; + break; + } if(sub_size>result) result=sub_size; } @@ -566,7 +580,7 @@ mp_integer compute_pointer_offset( mp_integer i; - if(sub_size!=0 && !to_integer(expr.op1(), i)) + if(sub_size>0 && !to_integer(expr.op1(), i)) return o+i*sub_size; } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index b1d070b85c9..ab25eb56a6a 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -383,12 +383,14 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr) if(ptr_expr.size()!=1 || int_expr.empty()) return true; - typet pointer_type=ptr_expr.front().type(); + typet pointer_sub_type=ptr_expr.front().type().subtype(); + if(pointer_sub_type.id()==ID_empty) + pointer_sub_type=char_type(); mp_integer element_size= - pointer_offset_size(pointer_type.subtype(), ns); + pointer_offset_size(pointer_sub_type, ns); - if(element_size==0) + if(element_size<0) return true; // this might change the type of the pointer!