CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
15static array_typet make_type(const irep_idt &value)
16{
19}
20
26
28{
29 exprt::type() = make_type(_value);
30 set(ID_value, _value);
31}
32
34{
35 return to_array_type(exprt::type());
36}
37
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
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
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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 std::string & get_string(const irep_idt &name) const
Definition irep.h:401
An expression without operands.
Definition std_expr.h:22
const array_typet & type() const
const typet & char_type() const
const irep_idt & value() const
array_exprt to_array_expr() const
convert string into array constant
string_constantt(const irep_idt &)
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)