Merge pull request #5760 from diffblue/floatbv_expr_h

move floating-point-related expression classes into separate header file

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/namespace.h>

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -23,6 +23,7 @@ Date:   April 2017
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/floatbv_expr.h>
 #include <util/fresh_symbol.h>
 #include <util/refined_string_type.h>
 #include <util/std_code.h>

scripts/expected_doxygen_warnings.txt

@@ -96,6 +96,6 @@ warning: Included by graph for 'namespace.h' not generated, too many nodes (112)
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), 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 (248), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (249), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (124), 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.

src/analyses/goto_check.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>

src/ansi-c/c_typecheck_expr.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>

src/ansi-c/expr2c.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/find_symbols.h>
 #include <util/fixedbv.h>
+#include <util/floatbv_expr.h>
 #include <util/lispexpr.h>
 #include <util/lispirep.h>
 #include <util/namespace.h>

src/goto-programs/adjust_float_expressions.cpp

@@ -11,12 +11,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "adjust_float_expressions.h"
 
+#include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
+#include <util/floatbv_expr.h>
+#include <util/ieee_float.h>
 #include <util/std_expr.h>
 #include <util/symbol.h>
-#include <util/ieee_float.h>
-#include <util/arith_tools.h>
 
 #include "goto_model.h"
 

src/solvers/flattening/boolbv.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/floatbv_expr.h>
 #include <util/magic.h>
 #include <util/mp_arith.h>
 #include <util/prefix.h>

src/solvers/flattening/boolbv.h

@@ -31,6 +31,8 @@ class bswap_exprt;
 class concatenation_exprt;
 class extractbit_exprt;
 class extractbits_exprt;
+class floatbv_typecast_exprt;
+class ieee_float_op_exprt;
 class member_exprt;
 class replication_exprt;
 

src/solvers/flattening/boolbv_floatbv_op.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <iostream>
 
+#include <util/floatbv_expr.h>
 #include <util/std_types.h>
 
 #include <solvers/floatbv/float_utils.h>

src/solvers/floatbv/float_bv.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/floatbv_expr.h>
 #include <util/std_expr.h>
 
 exprt float_bvt::convert(const exprt &expr) const

src/solvers/refinement/refine_arithmetic.cpp

@@ -8,10 +8,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "bv_refinement.h"
 
+#include <util/arith_tools.h>
 #include <util/bv_arithmetic.h>
-#include <util/ieee_float.h>
 #include <util/expr_util.h>
-#include <util/arith_tools.h>
+#include <util/floatbv_expr.h>
+#include <util/ieee_float.h>
 
 #include <solvers/floatbv/float_utils.h>
 

src/solvers/smt2/smt2_conv.h

@@ -13,8 +13,9 @@ Author: Daniel Kroening, [email protected]
 #include <sstream>
 #include <set>
 
-#include <util/std_expr.h>
 #include <util/byte_operators.h>
+#include <util/floatbv_expr.h>
+#include <util/std_expr.h>
 
 #if !HASH_CODE
 #  include <util/irep_hash_container.h>

src/solvers/smt2/smt2_parser.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>

src/solvers/strings/string_constraint_generator_float.cpp

@@ -14,6 +14,7 @@ Author: Romain Brenguier, [email protected]
 #include "string_constraint_generator.h"
 
 #include <util/bitvector_expr.h>
+#include <util/floatbv_expr.h>
 
 #include <solvers/floatbv/float_bv.h>