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