Skip to content

Commit

Permalink
Merge pull request diffblue#5898 from diffblue/move_bitvector_types
Browse files Browse the repository at this point in the history
Move bitvector types into util/bitvector_types.h
  • Loading branch information
kroening authored Mar 10, 2021
2 parents 8dd8dd3 + d30e826 commit 83ebd32
Show file tree
Hide file tree
Showing 86 changed files with 570 additions and 490 deletions.
6 changes: 3 additions & 3 deletions scripts/expected_doxygen_warnings.txt
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
Expand All @@ -35,6 +35,6 @@ warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (1
warning: Included by graph for 'prefix.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'std_expr.h' not generated, too many nodes (243), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'std_types.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'std_expr.h' not generated, too many nodes (241), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'std_types.h' not generated, too many nodes (102), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
3 changes: 3 additions & 0 deletions src/analyses/variable-sensitivity/abstract_value_object.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,11 @@
#include <analyses/variable-sensitivity/context_abstract_object.h>
#include <analyses/variable-sensitivity/interval_abstract_value.h>
#include <analyses/variable-sensitivity/value_set_abstract_object.h>

#include <goto-programs/adjust_float_expressions.h>

#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/ieee_float.h>
#include <util/make_unique.h>
#include <util/simplify_expr.h>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@
#include <limits.h>
#include <ostream>

#include <util/bitvector_types.h>
#include <util/invariant.h>
#include <util/make_unique.h>
#include <util/std_expr.h>

#include "abstract_environment.h"

Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/gcc_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_ANSI_C_GCC_TYPES_H
#define CPROVER_ANSI_C_GCC_TYPES_H

#include <util/std_types.h>
#include <util/bitvector_types.h>

// These are gcc-specific; most are not implemented by clang
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
Expand Down
3 changes: 2 additions & 1 deletion src/ansi-c/padding.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,11 @@ Author: Daniel Kroening, [email protected]

#include <algorithm>

#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/config.h>
#include <util/pointer_offset_size.h>
#include <util/simplify_expr.h>
#include <util/arith_tools.h>

mp_integer alignment(const typet &type, const namespacet &ns)
{
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/accelerate/util.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Author: Matt Lewis
#ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H
#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_UTIL_H

#include <util/std_types.h>
#include <util/bitvector_types.h>

signedbv_typet signed_poly_type();
unsignedbv_typet unsigned_poly_type();
Expand Down
1 change: 1 addition & 0 deletions src/goto-instrument/dump_c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]

#include "dump_c.h"

#include <util/bitvector_types.h>
#include <util/byte_operators.h>
#include <util/config.h>
#include <util/expr_initializer.h>
Expand Down
1 change: 1 addition & 0 deletions src/goto-instrument/stack_depth.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ Date: November 2011
#include "stack_depth.h"

#include <util/arith_tools.h>
#include <util/bitvector_types.h>

#include <goto-programs/goto_model.h>

Expand Down
1 change: 1 addition & 0 deletions src/goto-programs/goto_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Author: Daniel Kroening
#include <ostream>

#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/byte_operators.h>
#include <util/format_expr.h>
#include <util/merge_irep.h>
Expand Down
1 change: 1 addition & 0 deletions src/goto-programs/process_goto_program.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ Author: Martin Brain, [email protected]
#include <goto-programs/string_abstraction.h>
#include <goto-programs/string_instrumentation.h>

#include <util/bitvector_types.h>
#include <util/message.h>
#include <util/options.h>

Expand Down
3 changes: 2 additions & 1 deletion src/goto-programs/string_abstraction.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
#define CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H

#include <util/symbol_table.h>
#include <util/bitvector_types.h>
#include <util/config.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>

#include "goto_model.h"

Expand Down
1 change: 1 addition & 0 deletions src/goto-symex/partial_order_concurrency.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ Author: Michael Tautschnig, [email protected]
#include <limits>

#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/simplify_expr.h>

partial_order_concurrencyt::partial_order_concurrencyt(
Expand Down
3 changes: 2 additions & 1 deletion src/jsil/jsil_typecheck.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,10 @@ Author: Michael Tautschnig, [email protected]

#include "jsil_typecheck.h"

#include <util/symbol_table.h>
#include <util/bitvector_types.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>

#include "expr2jsil.h"
#include "jsil_types.h"
Expand Down
2 changes: 2 additions & 0 deletions src/jsil/jsil_types.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ Author: Daiva Naudziuniene, [email protected]

#include "jsil_types.h"

#include <util/bitvector_types.h>

#include <algorithm>

typet jsil_any_type()
Expand Down
1 change: 1 addition & 0 deletions src/solvers/flattening/boolbv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]

#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/floatbv_expr.h>
#include <util/magic.h>
#include <util/mp_arith.h>
Expand Down
4 changes: 2 additions & 2 deletions src/solvers/flattening/boolbv_abs.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,10 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <util/std_types.h>

#include "boolbv_type.h"

#include <util/bitvector_types.h>

#include <solvers/floatbv/float_utils.h>

bvt boolbvt::convert_abs(const abs_exprt &expr)
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_add_sub.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <util/bitvector_types.h>
#include <util/invariant.h>
#include <util/std_types.h>

#include <solvers/floatbv/float_utils.h>

Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_bv_rel.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <util/std_types.h>
#include <util/bitvector_types.h>

#include "boolbv_type.h"

Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_div.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <util/std_types.h>
#include <util/bitvector_types.h>

bvt boolbvt::convert_div(const div_exprt &expr)
{
Expand Down
1 change: 1 addition & 0 deletions src/solvers/flattening/boolbv_extractbit.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]

#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/exception_utils.h>
#include <util/std_expr.h>
#include <util/std_types.h>
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_floatbv_op.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@ Author: Daniel Kroening, [email protected]
#include <algorithm>
#include <iostream>

#include <util/bitvector_types.h>
#include <util/floatbv_expr.h>
#include <util/std_types.h>

#include <solvers/floatbv/float_utils.h>

Expand Down
4 changes: 2 additions & 2 deletions src/solvers/flattening/boolbv_ieee_float_rel.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,10 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <util/std_types.h>

#include "boolbv_type.h"

#include <util/bitvector_types.h>

#include <solvers/floatbv/float_utils.h>

literalt boolbvt::convert_ieee_float_rel(const binary_relation_exprt &expr)
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_mult.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <util/std_types.h>
#include <util/bitvector_types.h>

bvt boolbvt::convert_mult(const mult_exprt &expr)
{
Expand Down
3 changes: 2 additions & 1 deletion src/solvers/flattening/boolbv_not.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,10 @@ Author: Daniel Kroening, [email protected]
\*******************************************************************/


#include "boolbv.h"

#include <util/bitvector_types.h>

bvt boolbvt::convert_not(const not_exprt &expr)
{
const bvt &op_bv=convert_bv(expr.op());
Expand Down
3 changes: 2 additions & 1 deletion src/solvers/flattening/boolbv_reduction.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,10 @@ Author: Daniel Kroening, [email protected]
\*******************************************************************/


#include "boolbv.h"

#include <util/bitvector_types.h>

literalt boolbvt::convert_reduction(const unary_exprt &expr)
{
const bvt &op_bv=convert_bv(expr.op());
Expand Down
8 changes: 4 additions & 4 deletions src/solvers/flattening/boolbv_typecast.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,13 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <util/std_types.h>

#include <solvers/floatbv/float_utils.h>

#include "boolbv_type.h"
#include "c_bit_field_replacement_type.h"

#include <util/bitvector_types.h>

#include <solvers/floatbv/float_utils.h>

bvt boolbvt::convert_bv_typecast(const typecast_exprt &expr)
{
const exprt &op=expr.op();
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_unary_minus.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <util/std_types.h>
#include <util/bitvector_types.h>

#include <solvers/floatbv/float_utils.h>

Expand Down
1 change: 1 addition & 0 deletions src/solvers/flattening/c_bit_field_replacement_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]

#include "c_bit_field_replacement_type.h"

#include <util/bitvector_types.h>
#include <util/invariant.h>

typet c_bit_field_replacement_type(
Expand Down
1 change: 1 addition & 0 deletions src/solvers/floatbv/float_bv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]

#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/floatbv_expr.h>
#include <util/std_expr.h>

Expand Down
2 changes: 1 addition & 1 deletion src/solvers/lowering/popcount.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ Author: Michael Tautschnig

#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/invariant.h>
#include <util/pointer_offset_size.h>
#include <util/std_expr.h>

exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
{
Expand Down
1 change: 1 addition & 0 deletions src/solvers/refinement/refine_arithmetic.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
#include "bv_refinement.h"

#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/bv_arithmetic.h>
#include <util/expr_util.h>
#include <util/floatbv_expr.h>
Expand Down
3 changes: 1 addition & 2 deletions src/solvers/smt2/smt2_format.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,7 @@ Author: Daniel Kroening, [email protected]
#include "smt2_format.h"

#include <util/arith_tools.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/bitvector_types.h>

std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
{
Expand Down
1 change: 1 addition & 0 deletions src/solvers/smt2/smt2_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]

#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
Expand Down
5 changes: 3 additions & 2 deletions src/statement-list/converters/convert_dint_literal.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,11 @@ Author: Matthias Weiss, [email protected]
#include "convert_dint_literal.h"
#include "statement_list_types.h"

#include <util/arith_tools.h>
#include <util/bitvector_types.h>

#include <algorithm>
#include <stdexcept>
#include <util/arith_tools.h>
#include <util/std_types.h>

/// Minimum value of double integer literals.
#define STL_DINT_MAX_VALUE 2147483647LL
Expand Down
5 changes: 3 additions & 2 deletions src/statement-list/converters/convert_int_literal.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,11 @@ Author: Matthias Weiss, [email protected]
#include "convert_dint_literal.h"
#include "statement_list_types.h"

#include <util/arith_tools.h>
#include <util/bitvector_types.h>

#include <algorithm>
#include <stdexcept>
#include <util/arith_tools.h>
#include <util/std_types.h>

/// Maximum value of integer literals.
#define STL_INT_MAX_VALUE 32767LL
Expand Down
1 change: 1 addition & 0 deletions src/statement-list/converters/convert_real_literal.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Matthias Weiss, [email protected]
#include "convert_real_literal.h"
#include "statement_list_types.h"

#include <util/bitvector_types.h>
#include <util/ieee_float.h>
#include <util/std_expr.h>

Expand Down
3 changes: 2 additions & 1 deletion src/statement-list/converters/statement_list_types.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,9 @@ Author: Matthias Weiss, [email protected]
/// Statement List Type Helper

#include "statement_list_types.h"

#include <util/bitvector_types.h>
#include <util/ieee_float.h>
#include <util/std_types.h>

signedbv_typet get_int_type()
{
Expand Down
4 changes: 3 additions & 1 deletion src/statement-list/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,9 @@
#include "statement_list_parser.h"
#include "converters/convert_string_value.h"
#include "converters/statement_list_types.h"
#include <util/std_expr.h>

#include <util/bitvector_types.h>

#include <iterator>

int yystatement_listlex();
Expand Down
Loading

0 comments on commit 83ebd32

Please sign in to comment.