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/c_types.h>
12 #include <util/invariant.h>
13 
15  const c_bit_field_typet &src,
16  const namespacet &ns)
17 {
18  const typet &subtype=src.subtype();
19 
20  if(subtype.id()==ID_unsignedbv ||
21  subtype.id()==ID_signedbv ||
22  subtype.id()==ID_c_bool)
23  {
24  bitvector_typet result=to_bitvector_type(subtype);
25  result.set_width(src.get_width());
26  return std::move(result);
27  }
28  else
29  {
30  PRECONDITION(subtype.id() == ID_c_enum_tag);
31 
32  const typet &sub_subtype=
33  ns.follow_tag(to_c_enum_tag_type(subtype)).subtype();
34 
36  sub_subtype.id() == ID_signedbv || sub_subtype.id() == ID_unsignedbv);
37 
38  bitvector_typet result = to_bitvector_type(sub_subtype);
39  result.set_width(src.get_width());
40  return std::move(result);
41  }
42 }
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:28
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:66
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
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: c_types.h:19
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: c_types.h:317
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
irept::id
const irep_idt & id() const
Definition: irep.h:407
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:842
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:826
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:14
c_types.h