Skip to content

Commit 03c3c95

Browse files
authored
Merge pull request #7965 from diffblue/string-constant-types
string_constantt typing
2 parents eaa2cdd + cc0d810 commit 03c3c95

File tree

2 files changed

+44
-9
lines changed

2 files changed

+44
-9
lines changed

src/util/string_constant.cpp

Lines changed: 22 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,25 +12,40 @@ Author: Daniel Kroening, [email protected]
1212
#include "c_types.h"
1313
#include "std_expr.h"
1414

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+
1521
string_constantt::string_constantt(const irep_idt &_value)
16-
: nullary_exprt(ID_string_constant, typet())
22+
: nullary_exprt(ID_string_constant, make_type(_value))
1723
{
18-
set_value(_value);
24+
value(_value);
1925
}
2026

21-
void string_constantt::set_value(const irep_idt &value)
27+
void string_constantt::value(const irep_idt &_value)
2228
{
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);
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());
2641
}
2742

2843
/// convert string into array constant
2944
array_exprt string_constantt::to_array_expr() const
3045
{
3146
const std::string &str=get_string(ID_value);
3247
std::size_t string_size=str.size()+1; // we add the zero
33-
const typet &char_type = to_array_type(type()).element_type();
48+
const typet &char_type = string_constantt::char_type();
3449
bool char_is_unsigned=char_type.id()==ID_unsignedbv;
3550

3651
exprt size = from_integer(string_size, c_index_type());

src/util/string_constant.h

Lines changed: 22 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,16 +14,36 @@ Author: Daniel Kroening, [email protected]
1414
class string_constantt : public nullary_exprt
1515
{
1616
public:
17-
explicit string_constantt(const irep_idt &value);
17+
explicit string_constantt(const irep_idt &);
1818

19-
void set_value(const irep_idt &value);
19+
DEPRECATED(SINCE(2023, 10, 31, "use value(...)"))
20+
void set_value(const irep_idt &_value)
21+
{
22+
value(_value);
23+
}
24+
25+
void value(const irep_idt &);
2026

27+
DEPRECATED(SINCE(2023, 10, 31, "use value()"))
2128
const irep_idt &get_value() const
29+
{
30+
return value();
31+
}
32+
33+
const irep_idt &value() const
2234
{
2335
return get(ID_value);
2436
}
2537

2638
array_exprt to_array_expr() const;
39+
40+
const typet &char_type() const
41+
{
42+
return type().element_type();
43+
}
44+
45+
const array_typet &type() const;
46+
array_typet &type();
2747
};
2848

2949
template <>

0 commit comments

Comments
 (0)