cprover
c_types_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes
4 
5 Author: Malte Mues <mail.mues@gmail.com>
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_C_TYPES_UTIL_H
10 #define CPROVER_UTIL_C_TYPES_UTIL_H
11 
15 
16 #include "arith_tools.h"
17 #include "invariant.h"
18 #include "std_types.h"
19 #include "type.h"
20 
21 #include <algorithm>
22 #include <string>
23 
25 inline bool is_c_char_type(const typet &type)
26 {
27  const irep_idt &c_type = type.get(ID_C_c_type);
28  return is_signed_or_unsigned_bitvector(type) &&
29  (c_type == ID_char || c_type == ID_unsigned_char ||
30  c_type == ID_signed_char);
31 }
32 
35 inline bool is_c_bool_type(const typet &type)
36 {
37  return type.id() == ID_c_bool;
38 }
39 
44 inline bool is_c_integral_type(const typet &type)
45 {
46  const irep_idt &c_type = type.get(ID_C_c_type);
47  return is_signed_or_unsigned_bitvector(type) &&
48  (c_type == ID_signed_int || c_type == ID_unsigned_int ||
49  c_type == ID_signed_short_int || c_type == ID_unsigned_int ||
50  c_type == ID_unsigned_short_int || c_type == ID_signed_long_int ||
51  c_type == ID_signed_long_long_int || c_type == ID_unsigned_long_int ||
52  c_type == ID_unsigned_long_long_int);
53 }
54 
57 inline bool is_c_char_pointer_type(const typet &type)
58 {
59  return type.id() == ID_pointer && is_c_char_type(type.subtype());
60 }
61 
65 inline bool is_c_integral_pointer_type(const typet &type)
66 {
67  return type.id() == ID_pointer && is_c_integral_type(type.subtype());
68 }
69 
72 inline bool is_c_enum_type(const typet &type)
73 {
74  return type.id() == ID_c_enum;
75 }
76 
84  const irep_idt &member_name,
85  const c_enum_typet &c_enum)
86 {
87  for(const auto &enum_value : c_enum.members())
88  {
89  if(enum_value.get_identifier() == member_name)
90  {
91  auto maybe_int_value = numeric_cast<mp_integer>(
92  constant_exprt{enum_value.get_value(), typet{ID_bv}});
93  CHECK_RETURN(maybe_int_value.has_value());
94  return from_integer(*maybe_int_value, c_enum);
95  }
96  }
97  INVARIANT(false, "member_name must be a valid value in the c_enum.");
98 }
99 
103 inline bool id2boolean(const std::string &bool_value)
104 {
105  std::string string_value = bool_value;
106  std::transform(
107  string_value.begin(), string_value.end(), string_value.begin(), ::tolower);
108  if(string_value == "true")
109  return true;
110  if(string_value == "false")
111  return false;
112  UNREACHABLE;
113 }
114 
120 inline constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
121 {
122  return bool_value ? from_integer(mp_integer(1), type)
123  : from_integer(mp_integer(0), type);
124 }
125 #endif // CPROVER_UTIL_C_TYPES_UTIL_H
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
is_c_integral_pointer_type
bool is_c_integral_pointer_type(const typet &type)
This function checks, whether type is a pointer and the target type has been some kind of int type in...
Definition: c_types_util.h:65
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_enum_typet
The type of C enums.
Definition: std_types.h:620
arith_tools.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
convert_member_name_to_enum_value
constant_exprt convert_member_name_to_enum_value(const irep_idt &member_name, const c_enum_typet &c_enum)
This function creates a constant representing the bitvector encoded integer value of a string in the ...
Definition: c_types_util.h:83
from_c_boolean_value
constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
This function creates a constant representing either 0 or 1 as value of type type.
Definition: c_types_util.h:120
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
is_signed_or_unsigned_bitvector
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
Definition: std_types.h:1076
id2boolean
bool id2boolean(const std::string &bool_value)
Convert id to a Boolean value.
Definition: c_types_util.h:103
is_c_enum_type
bool is_c_enum_type(const typet &type)
This function checks, whether the type has been an enum type in the c program.
Definition: c_types_util.h:72
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
is_c_char_pointer_type
bool is_c_char_pointer_type(const typet &type)
This function checks, whether type is a pointer and the target type of the pointer has been a char ty...
Definition: c_types_util.h:57
is_c_char_type
bool is_c_char_type(const typet &type)
This function checks, whether this has been a char type in the c program.
Definition: c_types_util.h:25
std_types.h
Pre-defined types.
is_c_integral_type
bool is_c_integral_type(const typet &type)
This function checks, whether the type has been some kind of integer type in the c program.
Definition: c_types_util.h:44
irept::id
const irep_idt & id() const
Definition: irep.h:418
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
invariant.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
is_c_bool_type
bool is_c_bool_type(const typet &type)
This function checks, whether the type has been a bool type in the c program.
Definition: c_types_util.h:35
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
c_enum_typet::members
const memberst & members() const
Definition: std_types.h:646