File tree 3 files changed +6
-7
lines changed 3 files changed +6
-7
lines changed Original file line number Diff line number Diff line change @@ -11,6 +11,7 @@ Author: diffblue
11
11
12
12
#include " c_string_refinement.h"
13
13
#include " arith_tools.h"
14
+ #include " cprover_prefix.h"
14
15
#include " irep_ids.h"
15
16
#include " std_expr.h"
16
17
@@ -88,15 +89,15 @@ void c_string_refinementt::operator()(goto_functionst &goto_functions)
88
89
it != goto_functions.function_map .end ();
89
90
it++)
90
91
{
91
- if (it->first == " __CPROVER_math_func_string_index_of " )
92
+ if (it->first == CPROVER_PREFIX " math_func_string_index_of " )
92
93
{
93
94
do_string_index_of (it->second );
94
95
}
95
- else if (it->first == " __CPROVER_math_func_string_substring " )
96
+ else if (it->first == CPROVER_PREFIX " math_func_string_substring " )
96
97
{
97
98
do_string_substring (it->second );
98
99
}
99
- else if (it->first == " __CPROVER_math_func_string_concat " )
100
+ else if (it->first == CPROVER_PREFIX " math_func_string_concat " )
100
101
{
101
102
do_string_concat (it->second );
102
103
}
Original file line number Diff line number Diff line change @@ -42,7 +42,6 @@ string_constraint_generatort::add_axioms_for_index_of(
42
42
{
43
43
string_constraintst constraints;
44
44
const typet &index_type = from_index.type ();
45
- // const typet &size_type = str.length_type();
46
45
symbol_exprt index = fresh_symbol (" index_of" , index_type);
47
46
symbol_exprt contains = fresh_symbol (" contains_in_index_of" );
48
47
@@ -311,9 +310,9 @@ string_constraint_generatort::add_axioms_for_index_of(
311
310
PRECONDITION (args.size () == 2 || args.size () == 3 );
312
311
const array_string_exprt str = get_string_expr (array_pool, args[0 ]);
313
312
const exprt &c = args[1 ];
314
- const typet &index_type = f.type (); // str.length_type();
313
+ const typet &index_type = f.type ();
315
314
const typet &char_type = str.content ().type ().subtype ();
316
- // PRECONDITION(f.type() == index_type);
315
+
317
316
const exprt from_index =
318
317
args.size () == 2 ? from_integer (0 , index_type) : args[2 ];
319
318
Original file line number Diff line number Diff line change @@ -7,7 +7,6 @@ Author: Diffblue Ltd.
7
7
\*******************************************************************/
8
8
9
9
#include " string_refinement_util.h"
10
- #include " irep_ids.h"
11
10
#include " string_format_builtin_function.h"
12
11
#include < algorithm>
13
12
#include < functional>
You can’t perform that action at this time.
0 commit comments