Skip to content

Commit 33c34a0

Browse files
tautschnigtautschnig
authored
Merge pull request #3590 from tautschnig/string-constantt
Use string_constantt's API
2 parents 70287a1 + 72a025a commit 33c34a0

19 files changed

+59
-44
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ Author: Daniel Kroening, [email protected]
3232
#include <util/simplify_expr.h>
3333
#include <util/std_expr.h>
3434
#include <util/string2int.h>
35-
#include <util/string_constant.h>
3635
#include <util/threeval.h>
3736

3837
#include <goto-programs/cfg.h>

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/expr_util.h>
1515
#include <util/simplify_expr.h>
16+
#include <util/string_constant.h>
1617
#include <util/xml_expr.h>
1718

1819
#include <langapi/language_util.h>
@@ -182,10 +183,7 @@ unsigned custom_bitvector_analysist::get_bit_nr(
182183
else if(string_expr.id()==ID_index)
183184
return get_bit_nr(to_index_expr(string_expr).array());
184185
else if(string_expr.id()==ID_string_constant)
185-
{
186-
irep_idt value=string_expr.get(ID_value);
187-
return bits.number(value);
188-
}
186+
return bits.number(to_string_constant(string_expr).get_value());
189187
else
190188
return bits.number("(unknown)");
191189
}

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,13 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <cassert>
1515

16+
#include <util/arith_tools.h>
1617
#include <util/c_types.h>
1718
#include <util/config.h>
1819
#include <util/namespace.h>
1920
#include <util/simplify_expr.h>
20-
#include <util/arith_tools.h>
2121
#include <util/std_types.h>
22+
#include <util/string_constant.h>
2223

2324
#include "gcc_types.h"
2425

@@ -50,13 +51,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
5051
{
5152
if(type.has_subtype() &&
5253
type.subtype().id()==ID_string_constant)
53-
c_storage_spec.asm_label=type.subtype().get(ID_value);
54+
c_storage_spec.asm_label = to_string_constant(type.subtype()).get_value();
5455
}
5556
else if(type.id()==ID_section &&
5657
type.has_subtype() &&
5758
type.subtype().id()==ID_string_constant)
5859
{
59-
c_storage_spec.section=type.subtype().get(ID_value);
60+
c_storage_spec.section = to_string_constant(type.subtype()).get_value();
6061
}
6162
else if(type.id()==ID_const)
6263
c_qualifiers.is_constant=true;
@@ -230,7 +231,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
230231
type.has_subtype() &&
231232
type.subtype().id()==ID_string_constant)
232233
{
233-
c_storage_spec.alias=type.subtype().get(ID_value);
234+
c_storage_spec.alias = to_string_constant(type.subtype()).get_value();
234235
}
235236
else if(type.id()==ID_frontend_pointer)
236237
{

‎src/ansi-c/c_storage_spec.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "c_storage_spec.h"
1010

1111
#include <util/expr.h>
12+
#include <util/string_constant.h>
1213

1314
void c_storage_spect::read(const typet &type)
1415
{
@@ -50,18 +51,18 @@ void c_storage_spect::read(const typet &type)
5051
type.has_subtype() &&
5152
type.subtype().id()==ID_string_constant)
5253
{
53-
alias=type.subtype().get(ID_value);
54+
alias = to_string_constant(type.subtype()).get_value();
5455
}
5556
else if(type.id()==ID_asm &&
5657
type.has_subtype() &&
5758
type.subtype().id()==ID_string_constant)
5859
{
59-
asm_label=type.subtype().get(ID_value);
60+
asm_label = to_string_constant(type.subtype()).get_value();
6061
}
6162
else if(type.id()==ID_section &&
6263
type.has_subtype() &&
6364
type.subtype().id()==ID_string_constant)
6465
{
65-
section=type.subtype().get(ID_value);
66+
section = to_string_constant(type.subtype()).get_value();
6667
}
6768
}

‎src/ansi-c/expr2c.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
2424
#include <util/lispirep.h>
2525
#include <util/namespace.h>
2626
#include <util/pointer_offset_size.h>
27+
#include <util/string_constant.h>
2728
#include <util/suffix.h>
2829
#include <util/symbol.h>
2930

@@ -3867,7 +3868,8 @@ std::string expr2ct::convert_with_precedence(
38673868
return convert_constant(to_constant_expr(src), precedence);
38683869

38693870
else if(src.id()==ID_string_constant)
3870-
return '"'+MetaString(src.get_string(ID_value))+'"';
3871+
return '"' + MetaString(id2string(to_string_constant(src).get_value())) +
3872+
'"';
38713873

38723874
else if(src.id()==ID_struct)
38733875
return convert_struct(src, precedence);

‎src/ansi-c/literals/convert_string_literal.cpp

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -153,9 +153,6 @@ exprt convert_string_literal(const std::string &src)
153153
char_value[i]=value[i];
154154
}
155155

156-
string_constantt result;
157-
result.set_value(char_value);
158-
159-
return std::move(result);
156+
return string_constantt(char_value);
160157
}
161158
}

‎src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1388,8 +1388,7 @@ exprt cpp_typecheck_resolvet::resolve(
13881388
{
13891389
// __func__ is an ANSI-C standard compliant hack to get the function name
13901390
// __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
1391-
string_constantt s;
1392-
s.set_value(source_location.get_function());
1391+
string_constantt s(source_location.get_function());
13931392
s.add_source_location()=source_location;
13941393
return std::move(s);
13951394
}

‎src/cpp/cpp_typecheck_static_assert.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "cpp_typecheck.h"
1313

1414
#include <util/std_types.h>
15+
#include <util/string_constant.h>
1516

1617
void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert)
1718
{
@@ -31,7 +32,8 @@ void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert)
3132
error().source_location=cpp_static_assert.source_location();
3233
error() << "static assertion failed";
3334
if(cpp_static_assert.op1().id()==ID_string_constant)
34-
error() << ": " << cpp_static_assert.op1().get(ID_value);
35+
error() << ": "
36+
<< to_string_constant(cpp_static_assert.op1()).get_value();
3537
error() << eom;
3638
throw 0;
3739
}

‎src/goto-programs/goto_convert.cpp

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/prefix.h>
2121
#include <util/simplify_expr.h>
2222
#include <util/std_expr.h>
23+
#include <util/string_constant.h>
2324
#include <util/symbol_table.h>
2425
#include <util/symbol_table_builder.h>
2526

@@ -1819,7 +1820,10 @@ bool goto_convertt::get_string_constant(
18191820
simplify(index_op, ns);
18201821

18211822
if(index_op.id()==ID_string_constant)
1822-
return value=index_op.get(ID_value), false;
1823+
{
1824+
value = to_string_constant(index_op).get_value();
1825+
return false;
1826+
}
18231827
else if(index_op.id()==ID_array)
18241828
{
18251829
std::string result;
@@ -1839,7 +1843,10 @@ bool goto_convertt::get_string_constant(
18391843
}
18401844

18411845
if(expr.id()==ID_string_constant)
1842-
return value=expr.get(ID_value), false;
1846+
{
1847+
value = to_string_constant(expr).get_value();
1848+
return false;
1849+
}
18431850

18441851
return true;
18451852
}

‎src/goto-programs/string_abstraction.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
1818
#include <util/exception_utils.h>
1919
#include <util/expr_util.h>
2020
#include <util/pointer_predicates.h>
21+
#include <util/string_constant.h>
2122
#include <util/type_eq.h>
2223

2324
#include "pointer_arithmetic.h"
@@ -763,7 +764,8 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
763764

764765
if(object.id()==ID_string_constant)
765766
{
766-
const std::string &str_value = id2string(object.get(ID_value));
767+
const std::string &str_value =
768+
id2string(to_string_constant(object).get_value());
767769
// make sure we handle the case of a string constant with string-terminating
768770
// \0 in it
769771
const std::size_t str_len =

‎src/goto-programs/string_instrumentation.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/message.h>
2121
#include <util/std_code.h>
2222
#include <util/std_expr.h>
23+
#include <util/string_constant.h>
2324
#include <util/symbol_table.h>
2425

2526
#include <goto-programs/format_strings.h>
@@ -399,8 +400,8 @@ void string_instrumentationt::do_format_string_read(
399400
format_arg.op0().id()==ID_index &&
400401
format_arg.op0().op0().id()==ID_string_constant)
401402
{
402-
format_token_listt token_list=
403-
parse_format_string(format_arg.op0().op0().get_string(ID_value));
403+
format_token_listt token_list = parse_format_string(
404+
id2string(to_string_constant(format_arg.op0().op0()).get_value()));
404405

405406
std::size_t args=0;
406407

@@ -502,8 +503,8 @@ void string_instrumentationt::do_format_string_write(
502503
format_arg.op0().id()==ID_index &&
503504
format_arg.op0().op0().id()==ID_string_constant) // constant format
504505
{
505-
format_token_listt token_list=
506-
parse_format_string(format_arg.op0().op0().get_string(ID_value));
506+
format_token_listt token_list = parse_format_string(
507+
id2string(to_string_constant(format_arg.op0().op0()).get_value()));
507508

508509
std::size_t args=0;
509510

‎src/goto-symex/symex_builtin_functions.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
1919
#include <util/pointer_offset_size.h>
2020
#include <util/simplify_expr.h>
2121
#include <util/string2int.h>
22+
#include <util/string_constant.h>
2223

2324
inline static typet c_sizeof_type_rec(const exprt &expr)
2425
{
@@ -288,7 +289,7 @@ irep_idt get_string_argument_rec(const exprt &src)
288289
index_expr.index().is_zero())
289290
{
290291
const exprt &fmt_str = index_expr.array();
291-
return fmt_str.get_string(ID_value);
292+
return to_string_constant(fmt_str).get_value();
292293
}
293294
}
294295
}
@@ -476,7 +477,7 @@ void goto_symext::symex_trace(
476477
{
477478
std::list<exprt> vars;
478479

479-
irep_idt event=code.arguments()[1].op0().get(ID_value);
480+
irep_idt event = to_string_constant(code.arguments()[1].op0()).get_value();
480481

481482
for(std::size_t j=2; j<code.arguments().size(); j++)
482483
{

‎src/solvers/refinement/string_constraint_generator_constants.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Author: Romain Brenguier, [email protected]
1212
#include <solvers/refinement/string_constraint_generator.h>
1313

1414
#include <util/prefix.h>
15-
#include <util/string_constant.h>
1615
#include <util/unicode.h>
1716

1817
/// Add axioms ensuring that the provided string expression and constant are

‎src/solvers/refinement/string_constraint_generator_main.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -543,8 +543,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_char_literal(
543543
arg.op0().op0().operands().size()==2 &&
544544
arg.op0().op0().op0().id()==ID_string_constant)
545545
{
546-
const string_constantt s=to_string_constant(arg.op0().op0().op0());
547-
irep_idt sval=s.get_value();
546+
const string_constantt &s = to_string_constant(arg.op0().op0().op0());
547+
const std::string &sval = id2string(s.get_value());
548548
CHECK_RETURN(sval.size()==1);
549549
return {from_integer(unsigned(sval[0]), arg.type()), {}};
550550
}

‎src/util/format_constant.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,11 @@ Author: Daniel Kroening, [email protected]
1010
#include "format_constant.h"
1111

1212
#include "arith_tools.h"
13+
#include "expr.h"
1314
#include "fixedbv.h"
1415
#include "ieee_float.h"
15-
#include "expr.h"
1616
#include "std_expr.h"
17+
#include "string_constant.h"
1718

1819
std::string format_constantt::operator()(const exprt &expr)
1920
{
@@ -40,7 +41,7 @@ std::string format_constantt::operator()(const exprt &expr)
4041
}
4142
}
4243
else if(expr.id()==ID_string_constant)
43-
return expr.get_string(ID_value);
44+
return id2string(to_string_constant(expr).get_value());
4445

4546
return "(format-constant failed: "+expr.id_string()+")";
4647
}

‎src/util/simplify_expr_array.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
#include "pointer_offset_size.h"
1414
#include "replace_expr.h"
1515
#include "std_expr.h"
16+
#include "string_constant.h"
1617

1718
bool simplify_exprt::simplify_index(exprt &expr)
1819
{
@@ -137,7 +138,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
137138
{
138139
const auto i = numeric_cast<mp_integer>(expr.op1());
139140

140-
const irep_idt &value=array.get(ID_value);
141+
const std::string &value = id2string(to_string_constant(array).get_value());
141142

142143
if(!i.has_value())
143144
{

‎src/util/simplify_expr_pointer.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
1818
#include "pointer_offset_size.h"
1919
#include "pointer_predicates.h"
2020
#include "std_expr.h"
21+
#include "string_constant.h"
2122
#include "threeval.h"
2223

2324
static bool is_dereference_integer_object(
@@ -683,7 +684,8 @@ bool simplify_exprt::simplify_object_size(exprt &expr)
683684
else if(op.op0().id()==ID_string_constant)
684685
{
685686
typet type=expr.type();
686-
expr=from_integer(op.op0().get(ID_value).size()+1, type);
687+
expr =
688+
from_integer(to_string_constant(op.op0()).get_value().size() + 1, type);
687689
return false;
688690
}
689691
}

‎src/util/string_constant.cpp

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

15-
string_constantt::string_constantt() : nullary_exprt(ID_string_constant)
16-
{
17-
set_value(irep_idt());
18-
}
19-
2015
string_constantt::string_constantt(const irep_idt &_value)
2116
: nullary_exprt(ID_string_constant)
2217
{

‎src/util/string_constant.h

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
class string_constantt : public nullary_exprt
1616
{
1717
public:
18-
DEPRECATED("use string_constantt(value) instead")
19-
string_constantt();
20-
2118
explicit string_constantt(const irep_idt &value);
2219

2320
void set_value(const irep_idt &value);
@@ -37,10 +34,20 @@ inline const string_constantt &to_string_constant(const exprt &expr)
3734
return static_cast<const string_constantt &>(expr);
3835
}
3936

37+
inline const string_constantt &to_string_constant(const typet &type)
38+
{
39+
return to_string_constant((const exprt &)type);
40+
}
41+
4042
inline string_constantt &to_string_constant(exprt &expr)
4143
{
4244
PRECONDITION(expr.id() == ID_string_constant);
4345
return static_cast<string_constantt &>(expr);
4446
}
4547

48+
inline string_constantt &to_string_constant(typet &type)
49+
{
50+
return to_string_constant((exprt &)type);
51+
}
52+
4653
#endif // CPROVER_ANSI_C_STRING_CONSTANT_H

0 commit comments

Comments
 (0)