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 {
18 }
19 
21  : nullary_exprt(ID_string_constant)
22 {
23  set_value(_value);
24 }
25 
27 {
28  exprt size_expr=from_integer(value.size()+1, index_type());
29  type()=array_typet(char_type(), size_expr);
30  set(ID_value, value);
31 }
32 
35 {
36  const std::string &str=get_string(ID_value);
37  std::size_t string_size=str.size()+1; // we add the zero
39  bool char_is_unsigned=char_type.id()==ID_unsignedbv;
40 
41  exprt size=from_integer(string_size, index_type());
42 
43  array_exprt dest;
44  dest.type()=array_typet(char_type, size);
45 
46  dest.operands().resize(string_size);
47 
48  exprt::operandst::iterator it=dest.operands().begin();
49  for(std::size_t i=0; i<string_size; i++, it++)
50  {
51  // Are we at the end? Do implicit zero.
52  int ch=i==string_size-1?0:str[i];
53 
54  if(char_is_unsigned)
55  ch = (unsigned char)ch;
56  else
57  ch = (signed char)ch;
58 
59  *it = from_integer(ch, char_type);
60  }
61 
62  return dest;
63 }
The type of an expression, extends irept.
Definition: type.h:27
An expression without operands.
Definition: std_expr.h:23
void set_value(const irep_idt &value)
typet & type()
Return the type of the expression.
Definition: expr.h:68
const irep_idt & id() const
Definition: irep.h:259
API to expression classes.
array_exprt to_array_expr() const
convert string into array constant
size_t size() const
Definition: dstring.h:91
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:35
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
Arrays with given size.
Definition: std_types.h:1000
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:38
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet char_type()
Definition: c_types.cpp:114
Array constructor from list of elements.
Definition: std_expr.h:1739