diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index 5138cee161a3..0ca0e314e8a3 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -12,8 +12,11 @@ #include #include #include + #include + #include +#include #include #include #include diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 5fdeb8cd7034..857c9753d469 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -9,9 +9,9 @@ #include #include +#include #include #include -#include #include "abstract_environment.h" diff --git a/src/ansi-c/gcc_types.h b/src/ansi-c/gcc_types.h index 5da8d291cce3..0df39283d643 100644 --- a/src/ansi-c/gcc_types.h +++ b/src/ansi-c/gcc_types.h @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_GCC_TYPES_H #define CPROVER_ANSI_C_GCC_TYPES_H -#include +#include // These are gcc-specific; most are not implemented by clang // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index d300b182b3f1..b6691b2e139b 100644 --- a/src/ansi-c/padding.cpp +++ b/src/ansi-c/padding.cpp @@ -13,10 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include #include #include -#include mp_integer alignment(const typet &type, const namespacet &ns) { diff --git a/src/goto-instrument/accelerate/util.h b/src/goto-instrument/accelerate/util.h index 768a1b1bfe94..a72a55c96124 100644 --- a/src/goto-instrument/accelerate/util.h +++ b/src/goto-instrument/accelerate/util.h @@ -12,7 +12,7 @@ Author: Matt Lewis #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H -#include +#include signedbv_typet signed_poly_type(); unsignedbv_typet unsigned_poly_type(); diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 07f809660476..6fe778a03aee 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "dump_c.h" +#include #include #include #include diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 50371329fdd7..e87006c06eba 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -14,6 +14,7 @@ Date: November 2011 #include "stack_depth.h" #include +#include #include diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 1d9152571d94..55a08d146965 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening #include #include +#include #include #include #include diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 68121ab93354..5cbdc7288d71 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -26,6 +26,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include +#include #include #include diff --git a/src/goto-programs/string_abstraction.h b/src/goto-programs/string_abstraction.h index 7be6aa149897..049b8c1b7dbb 100644 --- a/src/goto-programs/string_abstraction.h +++ b/src/goto-programs/string_abstraction.h @@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H #define CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H -#include +#include #include #include +#include #include "goto_model.h" diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp index a4a2cbb6bc6c..e21fec68c6a9 100644 --- a/src/goto-symex/partial_order_concurrency.cpp +++ b/src/goto-symex/partial_order_concurrency.cpp @@ -14,6 +14,7 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk #include #include +#include #include partial_order_concurrencyt::partial_order_concurrencyt( diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index e8fe6623416b..d065485d21a0 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -11,9 +11,10 @@ Author: Michael Tautschnig, tautschn@amazon.com #include "jsil_typecheck.h" -#include +#include #include #include +#include #include "expr2jsil.h" #include "jsil_types.h" diff --git a/src/jsil/jsil_types.cpp b/src/jsil/jsil_types.cpp index ac2ff75c4878..6855ce540807 100644 --- a/src/jsil/jsil_types.cpp +++ b/src/jsil/jsil_types.cpp @@ -11,6 +11,8 @@ Author: Daiva Naudziuniene, daivan@amazon.com #include "jsil_types.h" +#include + #include typet jsil_any_type() diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 6c829d6ee6f3..3eece43679e5 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/src/solvers/flattening/boolbv_abs.cpp b/src/solvers/flattening/boolbv_abs.cpp index e43451f282e7..e5bbaa665b4e 100644 --- a/src/solvers/flattening/boolbv_abs.cpp +++ b/src/solvers/flattening/boolbv_abs.cpp @@ -8,10 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include - #include "boolbv_type.h" +#include + #include bvt boolbvt::convert_abs(const abs_exprt &expr) diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp index a3730867a3d0..de0e131e140a 100644 --- a/src/solvers/flattening/boolbv_add_sub.cpp +++ b/src/solvers/flattening/boolbv_add_sub.cpp @@ -8,8 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" +#include #include -#include #include diff --git a/src/solvers/flattening/boolbv_bv_rel.cpp b/src/solvers/flattening/boolbv_bv_rel.cpp index 86b9b88d3457..35febd35421d 100644 --- a/src/solvers/flattening/boolbv_bv_rel.cpp +++ b/src/solvers/flattening/boolbv_bv_rel.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include +#include #include "boolbv_type.h" diff --git a/src/solvers/flattening/boolbv_div.cpp b/src/solvers/flattening/boolbv_div.cpp index d8c0581fce5a..9ac5190359b5 100644 --- a/src/solvers/flattening/boolbv_div.cpp +++ b/src/solvers/flattening/boolbv_div.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include +#include bvt boolbvt::convert_div(const div_exprt &expr) { diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp index 77447217060e..4c5883bff3d7 100644 --- a/src/solvers/flattening/boolbv_extractbit.cpp +++ b/src/solvers/flattening/boolbv_extractbit.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp index dfbc38aae715..ace5a3a47bc9 100644 --- a/src/solvers/flattening/boolbv_floatbv_op.cpp +++ b/src/solvers/flattening/boolbv_floatbv_op.cpp @@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include #include diff --git a/src/solvers/flattening/boolbv_ieee_float_rel.cpp b/src/solvers/flattening/boolbv_ieee_float_rel.cpp index baa5a9f956d1..74fcb6042d42 100644 --- a/src/solvers/flattening/boolbv_ieee_float_rel.cpp +++ b/src/solvers/flattening/boolbv_ieee_float_rel.cpp @@ -8,10 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include - #include "boolbv_type.h" +#include + #include literalt boolbvt::convert_ieee_float_rel(const binary_relation_exprt &expr) diff --git a/src/solvers/flattening/boolbv_mult.cpp b/src/solvers/flattening/boolbv_mult.cpp index 6c5fc5537893..bababc98a6e9 100644 --- a/src/solvers/flattening/boolbv_mult.cpp +++ b/src/solvers/flattening/boolbv_mult.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include +#include bvt boolbvt::convert_mult(const mult_exprt &expr) { diff --git a/src/solvers/flattening/boolbv_not.cpp b/src/solvers/flattening/boolbv_not.cpp index 58c37e144830..d64e1c5df033 100644 --- a/src/solvers/flattening/boolbv_not.cpp +++ b/src/solvers/flattening/boolbv_not.cpp @@ -6,9 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #include "boolbv.h" +#include + bvt boolbvt::convert_not(const not_exprt &expr) { const bvt &op_bv=convert_bv(expr.op()); diff --git a/src/solvers/flattening/boolbv_reduction.cpp b/src/solvers/flattening/boolbv_reduction.cpp index ae9ef51ca578..655f56d0688e 100644 --- a/src/solvers/flattening/boolbv_reduction.cpp +++ b/src/solvers/flattening/boolbv_reduction.cpp @@ -6,9 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #include "boolbv.h" +#include + literalt boolbvt::convert_reduction(const unary_exprt &expr) { const bvt &op_bv=convert_bv(expr.op()); diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index 04355a22f69f..85c5764954a3 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -8,13 +8,13 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include - -#include - #include "boolbv_type.h" #include "c_bit_field_replacement_type.h" +#include + +#include + bvt boolbvt::convert_bv_typecast(const typecast_exprt &expr) { const exprt &op=expr.op(); diff --git a/src/solvers/flattening/boolbv_unary_minus.cpp b/src/solvers/flattening/boolbv_unary_minus.cpp index 375a6f62915d..3fde3d3258c2 100644 --- a/src/solvers/flattening/boolbv_unary_minus.cpp +++ b/src/solvers/flattening/boolbv_unary_minus.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include +#include #include diff --git a/src/solvers/flattening/c_bit_field_replacement_type.cpp b/src/solvers/flattening/c_bit_field_replacement_type.cpp index ad161d2b334d..07f7aa638af5 100644 --- a/src/solvers/flattening/c_bit_field_replacement_type.cpp +++ b/src/solvers/flattening/c_bit_field_replacement_type.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_bit_field_replacement_type.h" +#include #include typet c_bit_field_replacement_type( diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp index ad2ea004833d..c856a298db5c 100644 --- a/src/solvers/floatbv/float_bv.cpp +++ b/src/solvers/floatbv/float_bv.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include diff --git a/src/solvers/lowering/popcount.cpp b/src/solvers/lowering/popcount.cpp index 936a5189fc74..0cb340af3aee 100644 --- a/src/solvers/lowering/popcount.cpp +++ b/src/solvers/lowering/popcount.cpp @@ -10,9 +10,9 @@ Author: Michael Tautschnig #include #include +#include #include #include -#include exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns) { diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index 59d1ccdc6fb1..4a18871fdbcd 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "bv_refinement.h" #include +#include #include #include #include diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp index 99772d8d3544..08d3318778e4 100644 --- a/src/solvers/smt2/smt2_format.cpp +++ b/src/solvers/smt2/smt2_format.cpp @@ -9,8 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "smt2_format.h" #include -#include -#include +#include std::ostream &smt2_format_rec(std::ostream &out, const typet &type) { diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index a85f0c95b406..7dd3e42b4f3e 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/src/statement-list/converters/convert_dint_literal.cpp b/src/statement-list/converters/convert_dint_literal.cpp index 58a1dcbdda2c..302e625c1e81 100644 --- a/src/statement-list/converters/convert_dint_literal.cpp +++ b/src/statement-list/converters/convert_dint_literal.cpp @@ -12,10 +12,11 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include "convert_dint_literal.h" #include "statement_list_types.h" +#include +#include + #include #include -#include -#include /// Minimum value of double integer literals. #define STL_DINT_MAX_VALUE 2147483647LL diff --git a/src/statement-list/converters/convert_int_literal.cpp b/src/statement-list/converters/convert_int_literal.cpp index 4e3e6b134f1c..1728e9fde8ad 100644 --- a/src/statement-list/converters/convert_int_literal.cpp +++ b/src/statement-list/converters/convert_int_literal.cpp @@ -13,10 +13,11 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include "convert_dint_literal.h" #include "statement_list_types.h" +#include +#include + #include #include -#include -#include /// Maximum value of integer literals. #define STL_INT_MAX_VALUE 32767LL diff --git a/src/statement-list/converters/convert_real_literal.cpp b/src/statement-list/converters/convert_real_literal.cpp index 17c76075fafe..3738f0135d0a 100644 --- a/src/statement-list/converters/convert_real_literal.cpp +++ b/src/statement-list/converters/convert_real_literal.cpp @@ -12,6 +12,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include "convert_real_literal.h" #include "statement_list_types.h" +#include #include #include diff --git a/src/statement-list/converters/statement_list_types.cpp b/src/statement-list/converters/statement_list_types.cpp index d6ddc9ff4e20..f2ee5e84d185 100644 --- a/src/statement-list/converters/statement_list_types.cpp +++ b/src/statement-list/converters/statement_list_types.cpp @@ -10,8 +10,9 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com /// Statement List Type Helper #include "statement_list_types.h" + +#include #include -#include signedbv_typet get_int_type() { diff --git a/src/statement-list/parser.y b/src/statement-list/parser.y index 4cecf30438f9..1882612a908f 100644 --- a/src/statement-list/parser.y +++ b/src/statement-list/parser.y @@ -17,7 +17,9 @@ #include "statement_list_parser.h" #include "converters/convert_string_value.h" #include "converters/statement_list_types.h" -#include + +#include + #include int yystatement_listlex(); diff --git a/src/statement-list/statement_list_parse_tree_io.cpp b/src/statement-list/statement_list_parse_tree_io.cpp index 2719720b6a7b..b0abbb3cb3bf 100644 --- a/src/statement-list/statement_list_parse_tree_io.cpp +++ b/src/statement-list/statement_list_parse_tree_io.cpp @@ -13,6 +13,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include "converters/statement_list_types.h" #include +#include #include /// String to indicate that there is no value. diff --git a/src/util/Makefile b/src/util/Makefile index 2b722c9ada2f..256cddf6222b 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -4,6 +4,7 @@ SRC = allocate_objects.cpp \ array_name.cpp \ base_type.cpp \ bitvector_expr.cpp \ + bitvector_types.cpp \ bv_arithmetic.cpp \ byte_operators.cpp \ c_types.cpp \ diff --git a/src/util/bitvector_types.cpp b/src/util/bitvector_types.cpp new file mode 100644 index 000000000000..24e098fc2171 --- /dev/null +++ b/src/util/bitvector_types.cpp @@ -0,0 +1,56 @@ +/*******************************************************************\ + +Module: Pre-defined bitvector types + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Pre-defined bitvector types + +#include "bitvector_types.h" + +#include "arith_tools.h" +#include "bv_arithmetic.h" +#include "std_expr.h" +#include "string2int.h" + +std::size_t fixedbv_typet::get_integer_bits() const +{ + const irep_idt integer_bits = get(ID_integer_bits); + DATA_INVARIANT(!integer_bits.empty(), "integer bits should be set"); + return unsafe_string2unsigned(id2string(integer_bits)); +} + +std::size_t floatbv_typet::get_f() const +{ + const irep_idt &f = get(ID_f); + DATA_INVARIANT(!f.empty(), "the mantissa should be set"); + return unsafe_string2unsigned(id2string(f)); +} + +mp_integer integer_bitvector_typet::smallest() const +{ + return bv_spect(*this).min_value(); +} + +mp_integer integer_bitvector_typet::largest() const +{ + return bv_spect(*this).max_value(); +} + +constant_exprt integer_bitvector_typet::zero_expr() const +{ + return from_integer(0, *this); +} + +constant_exprt integer_bitvector_typet::smallest_expr() const +{ + return from_integer(smallest(), *this); +} + +constant_exprt integer_bitvector_typet::largest_expr() const +{ + return from_integer(largest(), *this); +} diff --git a/src/util/bitvector_types.h b/src/util/bitvector_types.h new file mode 100644 index 000000000000..4193031e5eb2 --- /dev/null +++ b/src/util/bitvector_types.h @@ -0,0 +1,382 @@ +/*******************************************************************\ + +Module: Pre-defined bitvector types + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Pre-defined bitvector types + +#ifndef CPROVER_UTIL_BITVECTOR_TYPES_H +#define CPROVER_UTIL_BITVECTOR_TYPES_H + +#include "std_types.h" + +/// This method tests, +/// if the given typet is a signed or unsigned bitvector. +inline bool is_signed_or_unsigned_bitvector(const typet &type) +{ + return type.id() == ID_signedbv || type.id() == ID_unsignedbv; +} + +/// \brief Cast a typet to a \ref bitvector_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// bitvector_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref bitvector_typet. +inline const bitvector_typet &to_bitvector_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + + return static_cast(type); +} + +/// \copydoc to_bitvector_type(const typet &type) +inline bitvector_typet &to_bitvector_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + + return static_cast(type); +} + +/// Fixed-width bit-vector without numerical interpretation +class bv_typet : public bitvector_typet +{ +public: + explicit bv_typet(std::size_t width) : bitvector_typet(ID_bv) + { + set_width(width); + } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, !type.get(ID_width).empty(), "bitvector type must have width"); + } +}; + +/// Check whether a reference to a typet is a \ref bv_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref bv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_bv; +} + +/// \brief Cast a typet to a \ref bv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// bv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref bv_typet. +inline const bv_typet &to_bv_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + bv_typet::check(type); + return static_cast(type); +} + +/// \copydoc to_bv_type(const typet &) +inline bv_typet &to_bv_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + bv_typet::check(type); + return static_cast(type); +} + +/// Fixed-width bit-vector representing a signed or unsigned integer +class integer_bitvector_typet : public bitvector_typet +{ +public: + integer_bitvector_typet(const irep_idt &id, std::size_t width) + : bitvector_typet(id, width) + { + } + + /// Return the smallest value that can be represented using this type. + mp_integer smallest() const; + /// Return the largest value that can be represented using this type. + mp_integer largest() const; + + // If we ever need any of the following three methods in \ref fixedbv_typet or + // \ref floatbv_typet, we might want to move them to a new class + // numeric_bitvector_typet, which would be between integer_bitvector_typet and + // bitvector_typet in the hierarchy. + + /// Return an expression representing the smallest value of this type. + constant_exprt smallest_expr() const; + /// Return an expression representing the zero value of this type. + constant_exprt zero_expr() const; + /// Return an expression representing the largest value of this type. + constant_exprt largest_expr() const; +}; + +/// Check whether a reference to a typet is an \ref integer_bitvector_typet. +/// \param type: Source type. +/// \return True if \p type is an \ref integer_bitvector_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_signedbv || type.id() == ID_unsignedbv; +} + +/// \brief Cast a typet to an \ref integer_bitvector_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// integer_bitvector_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref integer_bitvector_typet. +inline const integer_bitvector_typet & +to_integer_bitvector_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + + return static_cast(type); +} + +/// \copydoc to_integer_bitvector_type(const typet &type) +inline integer_bitvector_typet &to_integer_bitvector_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + + return static_cast(type); +} + +/// Fixed-width bit-vector with unsigned binary interpretation +class unsignedbv_typet : public integer_bitvector_typet +{ +public: + explicit unsignedbv_typet(std::size_t width) + : integer_bitvector_typet(ID_unsignedbv, width) + { + } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + bitvector_typet::check(type, vm); + } +}; + +/// Check whether a reference to a typet is a \ref unsignedbv_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref unsignedbv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_unsignedbv; +} + +/// \brief Cast a typet to an \ref unsignedbv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// unsignedbv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref unsignedbv_typet. +inline const unsignedbv_typet &to_unsignedbv_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + unsignedbv_typet::check(type); + return static_cast(type); +} + +/// \copydoc to_unsignedbv_type(const typet &) +inline unsignedbv_typet &to_unsignedbv_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + unsignedbv_typet::check(type); + return static_cast(type); +} + +/// Fixed-width bit-vector with two's complement interpretation +class signedbv_typet : public integer_bitvector_typet +{ +public: + explicit signedbv_typet(std::size_t width) + : integer_bitvector_typet(ID_signedbv, width) + { + } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, !type.get(ID_width).empty(), "signed bitvector type must have width"); + } +}; + +/// Check whether a reference to a typet is a \ref signedbv_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref signedbv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_signedbv; +} + +/// \brief Cast a typet to a \ref signedbv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// signedbv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref signedbv_typet. +inline const signedbv_typet &to_signedbv_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + signedbv_typet::check(type); + return static_cast(type); +} + +/// \copydoc to_signedbv_type(const typet &) +inline signedbv_typet &to_signedbv_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + signedbv_typet::check(type); + return static_cast(type); +} + +/// Fixed-width bit-vector with signed fixed-point interpretation +/// +/// Integer and fraction bits refer to the number of bits before and after +/// the decimal point, respectively. The width is the sum of the two. +class fixedbv_typet : public bitvector_typet +{ +public: + fixedbv_typet() : bitvector_typet(ID_fixedbv) + { + } + + std::size_t get_fraction_bits() const + { + return get_width() - get_integer_bits(); + } + + std::size_t get_integer_bits() const; + + void set_integer_bits(std::size_t b) + { + set(ID_integer_bits, narrow_cast(b)); + } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, !type.get(ID_width).empty(), "fixed bitvector type must have width"); + } +}; + +/// Check whether a reference to a typet is a \ref fixedbv_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref fixedbv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_fixedbv; +} + +/// \brief Cast a typet to a \ref fixedbv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// fixedbv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref fixedbv_typet. +inline const fixedbv_typet &to_fixedbv_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + fixedbv_typet::check(type); + return static_cast(type); +} + +/// \copydoc to_fixedbv_type(const typet &) +inline fixedbv_typet &to_fixedbv_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + fixedbv_typet::check(type); + return static_cast(type); +} + +/// Fixed-width bit-vector with IEEE floating-point interpretation +class floatbv_typet : public bitvector_typet +{ +public: + floatbv_typet() : bitvector_typet(ID_floatbv) + { + } + + std::size_t get_e() const + { + // subtract one for sign bit + return get_width() - get_f() - 1; + } + + std::size_t get_f() const; + + void set_f(std::size_t b) + { + set(ID_f, narrow_cast(b)); + } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, !type.get(ID_width).empty(), "float bitvector type must have width"); + } +}; + +/// Check whether a reference to a typet is a \ref floatbv_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref floatbv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_floatbv; +} + +/// \brief Cast a typet to a \ref floatbv_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// floatbv_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref floatbv_typet. +inline const floatbv_typet &to_floatbv_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + floatbv_typet::check(type); + return static_cast(type); +} + +/// \copydoc to_floatbv_type(const typet &) +inline floatbv_typet &to_floatbv_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + floatbv_typet::check(type); + return static_cast(type); +} + +#endif // CPROVER_UTIL_BITVECTOR_TYPES_H diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp index 94cbf1028700..c268975f74de 100644 --- a/src/util/bv_arithmetic.cpp +++ b/src/util/bv_arithmetic.cpp @@ -10,10 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "string2int.h" #include "arith_tools.h" -#include "std_types.h" +#include "bitvector_types.h" #include "std_expr.h" +#include "string2int.h" typet bv_spect::to_type() const { diff --git a/src/util/expr.cpp b/src/util/expr.cpp index c550b93221f1..509edbf08041 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format off #include "arith_tools.h" +#include "bitvector_types.h" #include "expr.h" #include "expr_iterator.h" #include "fixedbv.h" diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp index 489b500bf63e..813c41f96592 100644 --- a/src/util/fixedbv.cpp +++ b/src/util/fixedbv.cpp @@ -8,9 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "fixedbv.h" -#include "std_types.h" -#include "std_expr.h" #include "arith_tools.h" +#include "bitvector_types.h" +#include "std_expr.h" +#include "std_types.h" fixedbv_spect::fixedbv_spect(const fixedbv_typet &type) { diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 78be7e46b127..8b91e684cb06 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "arith_tools.h" +#include "bitvector_types.h" #include "invariant.h" #include "std_expr.h" #include "std_types.h" diff --git a/src/util/pointer_expr.h b/src/util/pointer_expr.h index 57c20749fb09..59f9ee004b7b 100644 --- a/src/util/pointer_expr.h +++ b/src/util/pointer_expr.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file util/pointer_expr.h /// API to expression classes for Pointers +#include "bitvector_types.h" #include "std_expr.h" class namespacet; diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp index 394ad55a58a6..f228ad448032 100644 --- a/src/util/simplify_expr_floatbv.cpp +++ b/src/util/simplify_expr_floatbv.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_class.h" #include "arith_tools.h" +#include "bitvector_types.h" #include "expr.h" #include "expr_util.h" #include "floatbv_expr.h" diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 62c7c72a3f5d..9f34fcdf6c3e 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -32,20 +32,6 @@ void array_typet::check(const typet &type, const validation_modet vm) } } -std::size_t fixedbv_typet::get_integer_bits() const -{ - const irep_idt integer_bits=get(ID_integer_bits); - DATA_INVARIANT(!integer_bits.empty(), "integer bits should be set"); - return unsafe_string2unsigned(id2string(integer_bits)); -} - -std::size_t floatbv_typet::get_f() const -{ - const irep_idt &f=get(ID_f); - DATA_INVARIANT(!f.empty(), "the mantissa should be set"); - return unsafe_string2unsigned(id2string(f)); -} - /// Return the sequence number of the component with given name. std::size_t struct_union_typet::component_number( const irep_idt &component_name) const @@ -177,31 +163,6 @@ mp_integer range_typet::get_to() const return string2integer(get_string(ID_to)); } -mp_integer integer_bitvector_typet::smallest() const -{ - return bv_spect(*this).min_value(); -} - -mp_integer integer_bitvector_typet::largest() const -{ - return bv_spect(*this).max_value(); -} - -constant_exprt integer_bitvector_typet::zero_expr() const -{ - return from_integer(0, *this); -} - -constant_exprt integer_bitvector_typet::smallest_expr() const -{ - return from_integer(smallest(), *this); -} - -constant_exprt integer_bitvector_typet::largest_expr() const -{ - return from_integer(largest(), *this); -} - /// Identify whether a given type is constant itself or contains constant /// components. /// Examples include: diff --git a/src/util/std_types.h b/src/util/std_types.h index 19245f2be9ef..dda86d086fed 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1078,371 +1078,6 @@ inline bool can_cast_type(const typet &type) type.id() == ID_c_bool; } -/// This method tests, -/// if the given typet is a signed or unsigned bitvector. -inline bool is_signed_or_unsigned_bitvector(const typet &type) -{ - return type.id() == ID_signedbv || type.id() == ID_unsignedbv; -} - -/// \brief Cast a typet to a \ref bitvector_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// bitvector_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref bitvector_typet. -inline const bitvector_typet &to_bitvector_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - - return static_cast(type); -} - -/// \copydoc to_bitvector_type(const typet &type) -inline bitvector_typet &to_bitvector_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - - return static_cast(type); -} - -/// Fixed-width bit-vector without numerical interpretation -class bv_typet:public bitvector_typet -{ -public: - explicit bv_typet(std::size_t width):bitvector_typet(ID_bv) - { - set_width(width); - } - - static void check( - const typet &type, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK( - vm, !type.get(ID_width).empty(), "bitvector type must have width"); - } -}; - -/// Check whether a reference to a typet is a \ref bv_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref bv_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_bv; -} - -/// \brief Cast a typet to a \ref bv_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// bv_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref bv_typet. -inline const bv_typet &to_bv_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - bv_typet::check(type); - return static_cast(type); -} - -/// \copydoc to_bv_type(const typet &) -inline bv_typet &to_bv_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - bv_typet::check(type); - return static_cast(type); -} - -/// Fixed-width bit-vector representing a signed or unsigned integer -class integer_bitvector_typet : public bitvector_typet -{ -public: - integer_bitvector_typet(const irep_idt &id, std::size_t width) - : bitvector_typet(id, width) - { - } - - /// Return the smallest value that can be represented using this type. - mp_integer smallest() const; - /// Return the largest value that can be represented using this type. - mp_integer largest() const; - - // If we ever need any of the following three methods in \ref fixedbv_typet or - // \ref floatbv_typet, we might want to move them to a new class - // numeric_bitvector_typet, which would be between integer_bitvector_typet and - // bitvector_typet in the hierarchy. - - /// Return an expression representing the smallest value of this type. - constant_exprt smallest_expr() const; - /// Return an expression representing the zero value of this type. - constant_exprt zero_expr() const; - /// Return an expression representing the largest value of this type. - constant_exprt largest_expr() const; -}; - -/// Check whether a reference to a typet is an \ref integer_bitvector_typet. -/// \param type: Source type. -/// \return True if \p type is an \ref integer_bitvector_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_signedbv || type.id() == ID_unsignedbv; -} - -/// \brief Cast a typet to an \ref integer_bitvector_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// integer_bitvector_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref integer_bitvector_typet. -inline const integer_bitvector_typet & -to_integer_bitvector_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - - return static_cast(type); -} - -/// \copydoc to_integer_bitvector_type(const typet &type) -inline integer_bitvector_typet &to_integer_bitvector_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - - return static_cast(type); -} - -/// Fixed-width bit-vector with unsigned binary interpretation -class unsignedbv_typet : public integer_bitvector_typet -{ -public: - explicit unsignedbv_typet(std::size_t width) - : integer_bitvector_typet(ID_unsignedbv, width) - { - } - - static void check( - const typet &type, - const validation_modet vm = validation_modet::INVARIANT) - { - bitvector_typet::check(type, vm); - } -}; - -/// Check whether a reference to a typet is a \ref unsignedbv_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref unsignedbv_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_unsignedbv; -} - -/// \brief Cast a typet to an \ref unsignedbv_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// unsignedbv_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref unsignedbv_typet. -inline const unsignedbv_typet &to_unsignedbv_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - unsignedbv_typet::check(type); - return static_cast(type); -} - -/// \copydoc to_unsignedbv_type(const typet &) -inline unsignedbv_typet &to_unsignedbv_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - unsignedbv_typet::check(type); - return static_cast(type); -} - -/// Fixed-width bit-vector with two's complement interpretation -class signedbv_typet : public integer_bitvector_typet -{ -public: - explicit signedbv_typet(std::size_t width) - : integer_bitvector_typet(ID_signedbv, width) - { - } - - static void check( - const typet &type, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK( - vm, !type.get(ID_width).empty(), "signed bitvector type must have width"); - } -}; - -/// Check whether a reference to a typet is a \ref signedbv_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref signedbv_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_signedbv; -} - -/// \brief Cast a typet to a \ref signedbv_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// signedbv_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref signedbv_typet. -inline const signedbv_typet &to_signedbv_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - signedbv_typet::check(type); - return static_cast(type); -} - -/// \copydoc to_signedbv_type(const typet &) -inline signedbv_typet &to_signedbv_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - signedbv_typet::check(type); - return static_cast(type); -} - -/// Fixed-width bit-vector with signed fixed-point interpretation -/// -/// Integer and fraction bits refer to the number of bits before and after -/// the decimal point, respectively. The width is the sum of the two. -class fixedbv_typet:public bitvector_typet -{ -public: - fixedbv_typet():bitvector_typet(ID_fixedbv) - { - } - - std::size_t get_fraction_bits() const - { - return get_width()-get_integer_bits(); - } - - std::size_t get_integer_bits() const; - - void set_integer_bits(std::size_t b) - { - set(ID_integer_bits, narrow_cast(b)); - } - - static void check( - const typet &type, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK( - vm, !type.get(ID_width).empty(), "fixed bitvector type must have width"); - } -}; - -/// Check whether a reference to a typet is a \ref fixedbv_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref fixedbv_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_fixedbv; -} - -/// \brief Cast a typet to a \ref fixedbv_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// fixedbv_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref fixedbv_typet. -inline const fixedbv_typet &to_fixedbv_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - fixedbv_typet::check(type); - return static_cast(type); -} - -/// \copydoc to_fixedbv_type(const typet &) -inline fixedbv_typet &to_fixedbv_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - fixedbv_typet::check(type); - return static_cast(type); -} - -/// Fixed-width bit-vector with IEEE floating-point interpretation -class floatbv_typet:public bitvector_typet -{ -public: - floatbv_typet():bitvector_typet(ID_floatbv) - { - } - - std::size_t get_e() const - { - // subtract one for sign bit - return get_width()-get_f()-1; - } - - std::size_t get_f() const; - - void set_f(std::size_t b) - { - set(ID_f, narrow_cast(b)); - } - - static void check( - const typet &type, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK( - vm, !type.get(ID_width).empty(), "float bitvector type must have width"); - } -}; - -/// Check whether a reference to a typet is a \ref floatbv_typet. -/// \param type: Source type. -/// \return True if \p type is a \ref floatbv_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_floatbv; -} - -/// \brief Cast a typet to a \ref floatbv_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// floatbv_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref floatbv_typet. -inline const floatbv_typet &to_floatbv_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - floatbv_typet::check(type); - return static_cast(type); -} - -/// \copydoc to_floatbv_type(const typet &) -inline floatbv_typet &to_floatbv_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - floatbv_typet::check(type); - return static_cast(type); -} - /// Type for C bit fields /// These are both 'bitvector_typet' (they have a width) /// and 'type_with_subtypet' (they have a subtype) diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp index cd31d5e620a2..fffd27f79d16 100644 --- a/unit/analyses/constant_propagator.cpp +++ b/unit/analyses/constant_propagator.cpp @@ -14,6 +14,7 @@ Author: Diffblue Ltd #include #include +#include #include #include diff --git a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp index 8e5f1b8ccca1..4362c11f76ec 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp @@ -4,9 +4,12 @@ #include #include #include -#include -#include -#include + +//#include +#include +//#include +//#include +//#include SCENARIO( "index_range for constant_abstract_values" diff --git a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp index 2c18baf656e9..870fe543db24 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp @@ -9,7 +9,8 @@ #include #include -#include + +#include SCENARIO( "merge_abstract_object", diff --git a/unit/analyses/variable-sensitivity/eval.cpp b/unit/analyses/variable-sensitivity/eval.cpp index 9234857b43af..08f0ab1146d1 100644 --- a/unit/analyses/variable-sensitivity/eval.cpp +++ b/unit/analyses/variable-sensitivity/eval.cpp @@ -3,8 +3,9 @@ #include #include #include + #include -#include +#include #include static symbolt simple_symbol(const irep_idt &identifier, const typet &type) diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp index ee2cfa82cbad..179cd642b7d9 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp @@ -13,6 +13,8 @@ #include #include +#include + SCENARIO( "meet_interval_abstract_value", "[core][analyses][variable-sensitivity][interval_abstract_value][meet]") diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp index c1f10c66aeda..2b8803ed156a 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -9,8 +9,9 @@ #include "analyses/variable-sensitivity/variable_sensitivity_test_helpers.h" #include #include + #include -#include +#include SCENARIO( "constants expression evaluation", diff --git a/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp b/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp index 6b829f417d67..9a27aba7dc12 100644 --- a/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp +++ b/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp @@ -7,15 +7,19 @@ Author: Diffblue Ltd. \*******************************************************************/ #include "value_set_test_common.h" + #include #include #include +#include + #include -#include +#include +#include + #include #include -#include #include namespace diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp index db6a7c68aad6..bce312fcad78 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp @@ -7,9 +7,13 @@ \*******************************************************************/ #include "../variable_sensitivity_test_helpers.h" + #include + #include + #include +#include #include SCENARIO( diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 31b6e1e756c6..52b7543b8772 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -7,9 +7,14 @@ \*******************************************************************/ #include "variable_sensitivity_test_helpers.h" + #include + #include + #include + +#include #include #include diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp index 710b03ada46a..c5d0573daf69 100644 --- a/unit/goto-programs/goto_program_assume.cpp +++ b/unit/goto-programs/goto_program_assume.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp index 7b591e892ed5..395a55e68cae 100644 --- a/unit/goto-programs/goto_program_dead.cpp +++ b/unit/goto-programs/goto_program_dead.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp index 00c16f58cf47..ab3d96f2082b 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index cb923f87cbfa..0ab493d20928 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index ebc9a571018c..ac23fa0edd38 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp index 9487fc5fd5c2..8f575edc7fa9 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp index c9ca127ba043..36207ce116c5 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/remove_returns.cpp b/unit/goto-programs/remove_returns.cpp index 4d782231d037..bc9d37b24c3b 100644 --- a/unit/goto-programs/remove_returns.cpp +++ b/unit/goto-programs/remove_returns.cpp @@ -11,9 +11,10 @@ Author: Diffblue Ltd. #include #include + +#include #include #include -#include #include TEST_CASE("Return-value removal", "[core][goto-programs][remove_returns]") diff --git a/unit/goto-programs/xml_expr.cpp b/unit/goto-programs/xml_expr.cpp index e4877eeb3a7f..dac9d3441112 100644 --- a/unit/goto-programs/xml_expr.cpp +++ b/unit/goto-programs/xml_expr.cpp @@ -9,10 +9,9 @@ Author: Michael Tautschnig #include #include +#include #include #include -#include -#include #include #include diff --git a/unit/goto-symex/is_constant.cpp b/unit/goto-symex/is_constant.cpp index a5af38d6843b..6f594d0e3ebc 100644 --- a/unit/goto-symex/is_constant.cpp +++ b/unit/goto-symex/is_constant.cpp @@ -10,8 +10,9 @@ Author: Diffblue Ltd. #include #include + +#include #include -#include SCENARIO("goto-symex-is-constant", "[core][goto-symex][is_constant]") { diff --git a/unit/goto-symex/ssa_equation.cpp b/unit/goto-symex/ssa_equation.cpp index f7c78dcd5d92..cb6d684ffa46 100644 --- a/unit/goto-symex/ssa_equation.cpp +++ b/unit/goto-symex/ssa_equation.cpp @@ -10,6 +10,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index fb6d3ca8dfba..a715228269ee 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -18,6 +18,7 @@ Author: Diffblue Ltd. #include #include +#include #include #include #include diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp index 39b49a639b82..d3c08c17477f 100644 --- a/unit/util/expr.cpp +++ b/unit/util/expr.cpp @@ -9,11 +9,10 @@ Author: Diffblue Ltd #include #include +#include #include -#include #include - SCENARIO("bitfield-expr-is-zero", "[core][util][expr]") { GIVEN("An exprt representing a bitfield constant of 3") diff --git a/unit/util/format.cpp b/unit/util/format.cpp index caf2d15139b0..dd6017662b48 100644 --- a/unit/util/format.cpp +++ b/unit/util/format.cpp @@ -6,6 +6,7 @@ \*******************************************************************/ +#include #include #include #include diff --git a/unit/util/interval/add.cpp b/unit/util/interval/add.cpp index 5ee1d0419b97..ae4923e89d1e 100644 --- a/unit/util/interval/add.cpp +++ b/unit/util/interval/add.cpp @@ -6,9 +6,8 @@ #include #include +#include #include -#include -#include #include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) diff --git a/unit/util/interval/bitwise.cpp b/unit/util/interval/bitwise.cpp index c738f1620ad6..d00f48564891 100644 --- a/unit/util/interval/bitwise.cpp +++ b/unit/util/interval/bitwise.cpp @@ -6,9 +6,8 @@ #include #include +#include #include -#include -#include #include SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]") diff --git a/unit/util/interval/comparisons.cpp b/unit/util/interval/comparisons.cpp index 15b3f1760b55..3e637a8a86d5 100644 --- a/unit/util/interval/comparisons.cpp +++ b/unit/util/interval/comparisons.cpp @@ -6,9 +6,8 @@ #include #include +#include #include -#include -#include #include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) diff --git a/unit/util/interval/divide.cpp b/unit/util/interval/divide.cpp index db436f9c2e6f..7d3e105ed469 100644 --- a/unit/util/interval/divide.cpp +++ b/unit/util/interval/divide.cpp @@ -4,9 +4,10 @@ \*******************************************************************/ #include + #include +#include #include -#include int value_of(const constant_interval_exprt &interval) { diff --git a/unit/util/interval/eval.cpp b/unit/util/interval/eval.cpp index 1a086f1ab18d..400d0373a505 100644 --- a/unit/util/interval/eval.cpp +++ b/unit/util/interval/eval.cpp @@ -5,11 +5,8 @@ #include -#include +#include #include -#include -#include -#include SCENARIO("Unary eval on intervals", "[core][analyses][interval][eval]") { diff --git a/unit/util/interval/get_extreme.cpp b/unit/util/interval/get_extreme.cpp index 71ada31d94a4..113ff8fd9c1b 100644 --- a/unit/util/interval/get_extreme.cpp +++ b/unit/util/interval/get_extreme.cpp @@ -6,11 +6,9 @@ #include #include +#include #include #include -#include -#include -#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) diff --git a/unit/util/interval/modulo.cpp b/unit/util/interval/modulo.cpp index 4c054917306d..dcd0e0bd6622 100644 --- a/unit/util/interval/modulo.cpp +++ b/unit/util/interval/modulo.cpp @@ -5,11 +5,8 @@ #include -#include +#include #include -#include -#include -#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) diff --git a/unit/util/interval/multiply.cpp b/unit/util/interval/multiply.cpp index 345abc20919d..97708d9b741d 100644 --- a/unit/util/interval/multiply.cpp +++ b/unit/util/interval/multiply.cpp @@ -5,11 +5,8 @@ #include -#include +#include #include -#include -#include -#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) diff --git a/unit/util/interval/shift.cpp b/unit/util/interval/shift.cpp index f2bebb74d95a..1b5bbb18ac78 100644 --- a/unit/util/interval/shift.cpp +++ b/unit/util/interval/shift.cpp @@ -5,11 +5,8 @@ #include -#include +#include #include -#include -#include -#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) diff --git a/unit/util/interval/subtract.cpp b/unit/util/interval/subtract.cpp index 16acd1d213a0..6944d34ec7f3 100644 --- a/unit/util/interval/subtract.cpp +++ b/unit/util/interval/subtract.cpp @@ -5,11 +5,8 @@ #include -#include +#include #include -#include -#include -#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) diff --git a/unit/util/interval/to_string.cpp b/unit/util/interval/to_string.cpp index ba90c54732e6..5e001e3c3b72 100644 --- a/unit/util/interval/to_string.cpp +++ b/unit/util/interval/to_string.cpp @@ -4,9 +4,9 @@ \*******************************************************************/ #include -#include + +#include #include -#include TEST_CASE("interval::to_string", "[core][analyses][interval]") { diff --git a/unit/util/interval_constraint.cpp b/unit/util/interval_constraint.cpp index 3a9192dbaa51..4b2f063ae34a 100644 --- a/unit/util/interval_constraint.cpp +++ b/unit/util/interval_constraint.cpp @@ -9,9 +9,9 @@ Author: Diffblue Ltd. #include +#include #include #include -#include SCENARIO( "interval_constraint with characters", diff --git a/unit/util/ssa_expr.cpp b/unit/util/ssa_expr.cpp index ec35114452a5..467fb711047e 100644 --- a/unit/util/ssa_expr.cpp +++ b/unit/util/ssa_expr.cpp @@ -9,8 +9,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include +#include #include -#include TEST_CASE("Constructor of ssa_exprt", "[unit][util][ssa_expr]") {