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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
typet::subtype
const typet & subtype() const
Definition: type.h:38
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:27
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
irep_idt
dstringt irep_idt
Definition: irep.h:32
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
string_constantt::string_constantt
string_constantt()
Definition: string_constant.cpp:15
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
nullary_exprt
An expression without operands.
Definition: std_expr.h:23
irept::id
const irep_idt & id() const
Definition: irep.h:259
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
string_constantt::to_array_expr
array_exprt to_array_expr() const
convert string into array constant
Definition: string_constant.cpp:34
array_typet
Arrays with given size.
Definition: std_types.h:1000
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
exprt::operands
operandst & operands()
Definition: expr.h:78
std_expr.h
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
c_types.h
string_constantt::set_value
void set_value(const irep_idt &value)
Definition: string_constant.cpp:26
dstringt::size
size_t size() const
Definition: dstring.h:91