cprover
Loading...
Searching...
No Matches
string_constant.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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, c_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, c_index_type());
37
38 array_exprt dest({}, array_typet(char_type, size));
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}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet char_type()
Definition: c_types.cpp:124
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Array constructor from list of elements.
Definition: std_expr.h:1476
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
size_t size() const
Definition: dstring.h:104
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
An expression without operands.
Definition: std_expr.h:22
string_constantt(const irep_idt &value)
array_exprt to_array_expr() const
convert string into array constant
void set_value(const irep_idt &value)
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:832