cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
15
static
array_typet
make_type
(
const
irep_idt
&value)
16
{
17
exprt
size_expr =
from_integer
(value.
size
() + 1,
c_index_type
());
18
return
array_typet
(
char_type
(), size_expr);
19
}
20
21
string_constantt::string_constantt
(
const
irep_idt
&_value)
22
:
nullary_exprt
(ID_string_constant,
make_type
(_value))
23
{
24
value
(_value);
25
}
26
27
void
string_constantt::value
(
const
irep_idt
&_value)
28
{
29
exprt::type
() =
make_type
(_value);
30
set
(ID_value, _value);
31
}
32
33
const
array_typet
&
string_constantt::type
()
const
34
{
35
return
to_array_type
(
exprt::type
());
36
}
37
38
array_typet
&
string_constantt::type
()
39
{
40
return
to_array_type
(
exprt::type
());
41
}
42
44
array_exprt
string_constantt::to_array_expr
()
const
45
{
46
const
std::string &str=
get_string
(ID_value);
47
std::size_t string_size=str.size()+1;
// we add the zero
48
const
typet
&
char_type
=
string_constantt::char_type
();
49
bool
char_is_unsigned=
char_type
.id()==ID_unsignedbv;
50
51
exprt
size =
from_integer
(string_size,
c_index_type
());
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
68
*it =
from_integer
(ch,
char_type
);
69
}
70
71
return
std::move(dest).with_source_location(*
this
);
72
}
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition
arith_tools.cpp:99
arith_tools.h
char_type
bitvector_typet char_type()
Definition
c_types.cpp:106
c_index_type
bitvector_typet c_index_type()
Definition
c_types.cpp:16
c_types.h
array_exprt
Array constructor from list of elements.
Definition
std_expr.h:1560
array_typet
Arrays with given size.
Definition
std_types.h:807
dstringt::size
size_t size() const
Definition
dstring.h:121
exprt
Base class for all expressions.
Definition
expr.h:57
exprt::exprt
exprt()
Definition
expr.h:62
exprt::type
typet & type()
Return the type of the expression.
Definition
expr.h:85
exprt::operands
operandst & operands()
Definition
expr.h:95
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition
irep.h:412
irept::get_string
const std::string & get_string(const irep_idt &name) const
Definition
irep.h:401
nullary_exprt::nullary_exprt
nullary_exprt(const irep_idt &_id, typet _type)
Definition
std_expr.h:25
string_constantt::type
const array_typet & type() const
Definition
string_constant.cpp:33
string_constantt::char_type
const typet & char_type() const
Definition
string_constant.h:28
string_constantt::value
const irep_idt & value() const
Definition
string_constant.h:21
string_constantt::to_array_expr
array_exprt to_array_expr() const
convert string into array constant
Definition
string_constant.cpp:44
string_constantt::string_constantt
string_constantt(const irep_idt &)
Definition
string_constant.cpp:21
typet
The type of an expression, extends irept.
Definition
type.h:29
std_expr.h
API to expression classes.
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition
std_types.h:888
make_type
static array_typet make_type(const irep_idt &value)
Definition
string_constant.cpp:15
string_constant.h
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
util
string_constant.cpp
Generated by
1.17.0