Merge pull request #5899 from diffblue/move_c_types

Move C types into util/c_types.h

Author: kroening

scripts/expected_doxygen_warnings.txt

@@ -22,7 +22,7 @@ warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, to
 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 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'c_types.h' not generated, too many nodes (141), 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.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
@@ -31,10 +31,10 @@ warning: Included by graph for 'invariant.h' not generated, too many nodes (186)
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 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 (79), 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 (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 'std_types.h' not generated, too many nodes (96), 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/ansi-c/c_typecheck_base.h

@@ -13,10 +13,10 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANSI_C_C_TYPECHECK_BASE_H
 
 #include <util/bitvector_expr.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
-#include <util/std_types.h>
 #include <util/symbol_table.h>
 #include <util/typecheck.h>
 

src/ansi-c/padding.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
-#include <util/bitvector_types.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>

src/ansi-c/type2name.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "type2name.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>

src/cpp/cpp_exception_id.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_exception_id.h"
 
+#include <util/c_types.h>
 #include <util/invariant.h>
 #include <util/std_types.h>
 

src/cpp/expr2cpp.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr2cpp.h"
 
+#include <util/c_types.h>
 #include <util/lispexpr.h>
 #include <util/lispirep.h>
 #include <util/namespace.h>

src/goto-instrument/dump_c.cpp

@@ -11,8 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "dump_c.h"
 
-#include <util/bitvector_types.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_initializer.h>
 #include <util/find_symbols.h>

src/goto-programs/goto_trace.cpp

@@ -16,8 +16,8 @@ Author: Daniel Kroening
 #include <ostream>
 
 #include <util/arith_tools.h>
-#include <util/bitvector_types.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/format_expr.h>
 #include <util/merge_irep.h>
 #include <util/range.h>

src/goto-programs/interpreter.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <cstring>
 
+#include <util/c_types.h>
 #include <util/fixedbv.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>

src/goto-programs/interpreter_evaluate.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/fixedbv.h>
 #include <util/ieee_float.h>
 #include <util/pointer_expr.h>

src/goto-programs/json_expr.cpp

@@ -12,6 +12,7 @@ Author: Peter Schrammel
 #include "json_expr.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr.h>
 #include <util/expr_util.h>

src/goto-programs/xml_expr.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening
 #include "xml_expr.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr.h>
 #include <util/fixedbv.h>

src/goto-symex/goto_symex_state.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/as_const.h>
 #include <util/base_exceptions.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/format.h>

src/jsil/jsil_types.h

@@ -12,8 +12,7 @@ Author: Daiva Naudziuniene, [email protected]
 #ifndef CPROVER_JSIL_JSIL_TYPES_H
 #define CPROVER_JSIL_JSIL_TYPES_H
 
-#include <util/type.h>
-#include <util/std_types.h>
+#include <util/c_types.h>
 
 typet jsil_kind();
 typet jsil_any_type();

src/linking/linking.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_set>
 
 #include <util/base_type.h>
+#include <util/c_types.h>
 #include <util/find_symbols.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_expr.h>

src/solvers/flattening/boolbv_update.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "boolbv.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 
 bvt boolbvt::convert_update(const update_exprt &expr)
 {

src/solvers/flattening/boolbv_width.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/namespace.h>

src/solvers/flattening/boolbv_with.cpp

@@ -8,10 +8,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/std_types.h>
-#include <util/std_expr.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 
 bvt boolbvt::convert_with(const with_exprt &expr)
 {

src/solvers/flattening/c_bit_field_replacement_type.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_bit_field_replacement_type.h"
 
-#include <util/bitvector_types.h>
+#include <util/c_types.h>
 #include <util/invariant.h>
 
 typet c_bit_field_replacement_type(

src/solvers/flattening/c_bit_field_replacement_type.h

@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H
 #define CPROVER_SOLVERS_FLATTENING_C_BIT_FIELD_REPLACEMENT_TYPE_H
 
-#include <util/std_types.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
 
 typet c_bit_field_replacement_type(

src/solvers/smt2/smt2_conv.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <set>
 
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/floatbv_expr.h>
 #include <util/std_expr.h>
 

src/util/arith_tools.cpp

@@ -8,10 +8,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "arith_tools.h"
 
+#include "c_types.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "invariant.h"
-#include "pointer_expr.h"
 #include "std_expr.h"
 #include "std_types.h"
 

src/util/c_types.cpp

@@ -6,12 +6,12 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include "c_types.h"
 
-#include "std_types.h"
 #include "config.h"
 #include "invariant.h"
-
-#include "c_types.h"
+#include "pointer_offset_size.h"
+#include "std_types.h"
 
 bitvector_typet index_type()
 {
@@ -303,3 +303,34 @@ std::string c_type_as_string(const irep_idt &c_type)
   else
     return "";
 }
+
+optionalt<std::pair<struct_union_typet::componentt, mp_integer>>
+union_typet::find_widest_union_component(const namespacet &ns) const
+{
+  const union_typet::componentst &comps = components();
+
+  optionalt<mp_integer> max_width;
+  typet max_comp_type;
+  irep_idt max_comp_name;
+
+  for(const auto &comp : comps)
+  {
+    auto element_width = pointer_offset_bits(comp.type(), ns);
+
+    if(!element_width.has_value())
+      return {};
+
+    if(max_width.has_value() && *element_width <= *max_width)
+      continue;
+
+    max_width = *element_width;
+    max_comp_type = comp.type();
+    max_comp_name = comp.get_name();
+  }
+
+  if(!max_width.has_value())
+    return {};
+  else
+    return std::make_pair(
+      struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width);
+}