CBMC
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 
15 static array_typet make_type(const irep_idt &value)
16 {
17  exprt size_expr = from_integer(value.size() + 1, c_index_type());
18  return array_typet(char_type(), size_expr);
19 }
20 
22  : nullary_exprt(ID_string_constant, make_type(_value))
23 {
24  value(_value);
25 }
26 
27 void string_constantt::value(const irep_idt &_value)
28 {
29  exprt::type() = make_type(_value);
30  set(ID_value, _value);
31 }
32 
34 {
35  return to_array_type(exprt::type());
36 }
37 
39 {
40  return to_array_type(exprt::type());
41 }
42 
45 {
46  const std::string &str=get_string(ID_value);
47  std::size_t string_size=str.size()+1; // we add the zero
49  bool char_is_unsigned=char_type.id()==ID_unsignedbv;
50 
51  exprt size = from_integer(string_size, c_index_type());
52 
53  array_exprt dest({}, array_typet(char_type, size));
54 
55  dest.operands().resize(string_size);
56 
57  exprt::operandst::iterator it=dest.operands().begin();
58  for(std::size_t i=0; i<string_size; i++, it++)
59  {
60  // Are we at the end? Do implicit zero.
61  int ch=i==string_size-1?0:str[i];
62 
63  if(char_is_unsigned)
64  ch = (unsigned char)ch;
65  else
66  ch = (signed char)ch;
67 
68  *it = from_integer(ch, char_type);
69  }
70 
71  return std::move(dest).with_source_location(*this);
72 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet char_type()
Definition: c_types.cpp:106
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Array constructor from list of elements.
Definition: std_expr.h:1621
Arrays with given size.
Definition: std_types.h:807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
size_t size() const
Definition: dstring.h:121
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
const irep_idt & id() const
Definition: irep.h:388
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:401
An expression without operands.
Definition: std_expr.h:22
const irep_idt & value() const
const array_typet & type() const
array_exprt to_array_expr() const
convert string into array constant
string_constantt(const irep_idt &)
const typet & char_type() const
The type of an expression, extends irept.
Definition: type.h:29
API to expression classes.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
static array_typet make_type(const irep_idt &value)