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  : nullary_exprt(ID_string_constant, typet())
17 {
18  set_value(_value);
19 }
20 
22 {
23  exprt size_expr=from_integer(value.size()+1, index_type());
24  type()=array_typet(char_type(), size_expr);
25  set(ID_value, value);
26 }
27 
30 {
31  const std::string &str=get_string(ID_value);
32  std::size_t string_size=str.size()+1; // we add the zero
34  bool char_is_unsigned=char_type.id()==ID_unsignedbv;
35 
36  exprt size=from_integer(string_size, index_type());
37 
39 
40  dest.operands().resize(string_size);
41 
42  exprt::operandst::iterator it=dest.operands().begin();
43  for(std::size_t i=0; i<string_size; i++, it++)
44  {
45  // Are we at the end? Do implicit zero.
46  int ch=i==string_size-1?0:str[i];
47 
48  if(char_is_unsigned)
49  ch = (unsigned char)ch;
50  else
51  ch = (signed char)ch;
52 
53  *it = from_integer(ch, char_type);
54  }
55 
56  return dest;
57 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
string_constantt::string_constantt
string_constantt(const irep_idt &value)
Definition: string_constant.cpp:15
arith_tools.h
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
typet
The type of an expression, extends irept.
Definition: type.h:29
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
nullary_exprt
An expression without operands.
Definition: std_expr.h:24
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:431
string_constantt::to_array_expr
array_exprt to_array_expr() const
convert string into array constant
Definition: string_constant.cpp:29
array_typet
Arrays with given size.
Definition: std_types.h:965
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
exprt::operands
operandst & operands()
Definition: expr.h:95
std_expr.h
API to expression classes.
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
c_types.h
string_constantt::set_value
void set_value(const irep_idt &value)
Definition: string_constant.cpp:21
dstringt::size
size_t size() const
Definition: dstring.h:104