cprover
string_constant.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "string_constant.h"
10 
11 #include "arith_tools.h"
12 #include "c_types.h"
13 #include "std_expr.h"
14 
16  exprt(ID_string_constant)
17 {
19 }
20 
22  exprt(ID_string_constant)
23 {
24  set_value(_value);
25 }
26 
28 {
29  exprt size_expr=from_integer(value.size()+1, index_type());
30  type()=array_typet(char_type(), size_expr);
31  set(ID_value, value);
32 }
33 
36 {
37  const std::string &str=get_string(ID_value);
38  std::size_t string_size=str.size()+1; // we add the zero
39  const typet &char_type=type().subtype();
40  bool char_is_unsigned=char_type.id()==ID_unsignedbv;
41 
42  exprt size=from_integer(string_size, index_type());
43 
44  array_exprt dest;
45  dest.type()=array_typet(char_type, size);
46 
47  dest.operands().resize(string_size);
48 
49  exprt::operandst::iterator it=dest.operands().begin();
50  for(std::size_t i=0; i<string_size; i++, it++)
51  {
52  // Are we at the end? Do implicit zero.
53  int ch=i==string_size-1?0:str[i];
54 
55  if(char_is_unsigned)
56  ch=(unsigned char)ch;
57 
58  exprt &op=*it;
59 
60  op=from_integer(ch, char_type);
61 
62  if(ch>=32 && ch<=126)
63  {
64  std::string ch_str="'";
65  if(ch=='\'' || ch=='\\')
66  ch_str+='\\';
67  ch_str+=static_cast<char>(ch);
68  ch_str+="'";
69  }
70  }
71 
72  return dest;
73 }
74 
78 {
79  id(ID_string_constant);
80  type()=src.type();
81 
82  const typet &subtype=type().subtype();
83 
84  // check subtype
85  if(subtype!=signed_char_type() &&
86  subtype!=unsigned_char_type())
87  return true;
88 
89  std::string value;
90 
91  forall_operands(it, src)
92  {
93  mp_integer int_value=0;
94  if(to_integer(*it, int_value))
95  return true;
96  unsigned unsigned_value=integer2unsigned(int_value);
97  value+=static_cast<char>(unsigned_value);
98  }
99 
100  // Drop the implicit zero at the end.
101  // Not clear what the semantics should be if it's not there.
102  if(!value.empty() && value[value.size()-1]==0)
103  value.resize(value.size()-1);
104 
105  set_value(value);
106 
107  return false;
108 }
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
void set_value(const irep_idt &value)
bool from_array_expr(const array_exprt &)
convert array constant into string
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:259
API to expression classes.
#define forall_operands(it, expr)
Definition: expr.h:17
array_exprt to_array_expr() const
convert string into array constant
size_t size() const
Definition: dstring.h:89
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
Base class for all expressions.
Definition: expr.h:42
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
arrays with given size
Definition: std_types.h:1013
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
dstringt irep_idt
Definition: irep.h:32
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
bitvector_typet char_type()
Definition: c_types.cpp:114
array constructor from list of elements
Definition: std_expr.h:1617