11
11
12
12
#include < solvers/refinement/string_refinement_invariant.h>
13
13
#include < solvers/refinement/string_constraint_generator.h>
14
+ #include < util/deprecation.h>
14
15
15
16
// / Add axioms ensuring the result `res` corresponds to `s1` where we
16
17
// / inserted `s2` at position `offset`.
@@ -130,6 +131,7 @@ exprt string_constraint_generatort::add_axioms_for_insert(
130
131
// / \param f: function application with three arguments: a string, an
131
132
// / integer offset, and an integer
132
133
// / \return an expression
134
+ DEPRECATED (" " )
133
135
exprt string_constraint_generatort::add_axioms_for_insert_int(
134
136
const function_application_exprt &f)
135
137
{
@@ -150,6 +152,7 @@ exprt string_constraint_generatort::add_axioms_for_insert_int(
150
152
// / \param f: function application with three arguments: a string, an
151
153
// / integer offset, and a Boolean
152
154
// / \return a new string expression
155
+ DEPRECATED (" should convert the value to string and call insert" )
153
156
exprt string_constraint_generatort::add_axioms_for_insert_bool(
154
157
const function_application_exprt &f)
155
158
{
@@ -190,6 +193,7 @@ exprt string_constraint_generatort::add_axioms_for_insert_char(
190
193
// / \param f: function application with three arguments: a string, an
191
194
// / integer offset, and a double
192
195
// / \return a string expression
196
+ DEPRECATED (" should convert the value to string and call insert" )
193
197
exprt string_constraint_generatort::add_axioms_for_insert_double(
194
198
const function_application_exprt &f)
195
199
{
@@ -211,6 +215,7 @@ exprt string_constraint_generatort::add_axioms_for_insert_double(
211
215
// / \param f: function application with three arguments: a string, an
212
216
// / integer offset, and a float
213
217
// / \return a new string expression
218
+ DEPRECATED (" should convert the value to string and call insert" )
214
219
exprt string_constraint_generatort::add_axioms_for_insert_float(
215
220
const function_application_exprt &f)
216
221
{
0 commit comments