cprover
c_bit_field_replacement_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <util/invariant.h>
12 
14  const c_bit_field_typet &src,
15  const namespacet &ns)
16 {
17  const typet &subtype=src.subtype();
18 
19  if(subtype.id()==ID_unsignedbv ||
20  subtype.id()==ID_signedbv ||
21  subtype.id()==ID_c_bool)
22  {
23  bitvector_typet result=to_bitvector_type(subtype);
24  result.set_width(src.get_width());
25  return std::move(result);
26  }
27  else
28  {
29  PRECONDITION(subtype.id() == ID_c_enum_tag);
30 
31  const typet &sub_subtype=
32  ns.follow_tag(to_c_enum_tag_type(subtype)).subtype();
33 
35  sub_subtype.id() == ID_signedbv || sub_subtype.id() == ID_unsignedbv);
36 
37  bitvector_typet result = to_bitvector_type(sub_subtype);
38  result.set_width(src.get_width());
39  return std::move(result);
40  }
41 }
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:721
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_bit_field_replacement_type.h
typet
The type of an expression, extends irept.
Definition: type.h:29
invariant.h
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
c_bit_field_typet
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: std_types.h:1443
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
irept::id
const irep_idt & id() const
Definition: irep.h:418
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:1046
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:1030
c_bit_field_replacement_type
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
Definition: c_bit_field_replacement_type.cpp:13
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089