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 
9 
11 
13  const c_bit_field_typet &src,
14  const namespacet &ns)
15 {
16  const typet &subtype=src.subtype();
17 
18  if(subtype.id()==ID_unsignedbv ||
19  subtype.id()==ID_signedbv ||
20  subtype.id()==ID_c_bool)
21  {
22  bitvector_typet result=to_bitvector_type(subtype);
23  result.set_width(src.get_width());
24  return std::move(result);
25  }
26  else if(subtype.id()==ID_c_enum_tag)
27  {
28  const typet &sub_subtype=
29  ns.follow_tag(to_c_enum_tag_type(subtype)).subtype();
30 
31  if(sub_subtype.id()==ID_signedbv ||
32  sub_subtype.id()==ID_unsignedbv)
33  {
34  bitvector_typet result=to_bitvector_type(sub_subtype);
35  result.set_width(src.get_width());
36  return std::move(result);
37  }
38  else
39  return nil_typet();
40  }
41  else
42  return nil_typet();
43 }
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:737
typet::subtype
const typet & subtype() const
Definition: type.h:38
c_bit_field_replacement_type.h
typet
The type of an expression, extends irept.
Definition: type.h:27
nil_typet
The NIL type, i.e., an invalid type, no value.
Definition: std_types.h:39
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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:1462
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
irept::id
const irep_idt & id() const
Definition: irep.h:259
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:1122
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:1105
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:12
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158