File tree 2 files changed +5
-8
lines changed
2 files changed +5
-8
lines changed Original file line number Diff line number Diff line change @@ -29,22 +29,23 @@ refined_string_typet::refined_string_typet(
29
29
array_typet char_array (char_type, infinite_index);
30
30
components ().emplace_back (" length" , index_type);
31
31
components ().emplace_back (" content" , char_array);
32
+ set_tag (CPROVER_PREFIX" refined_string_type" );
32
33
}
33
34
34
35
/* ******************************************************************\
35
36
36
- Function: refined_string_typet::is_c_string_type
37
+ Function: refined_string_typet::is_refined_string_type
37
38
38
39
Inputs: a type
39
40
40
- Outputs: Boolean telling whether the type is that of C strings
41
+ Outputs: Boolean telling whether the input is a refined string type
41
42
42
43
\*******************************************************************/
43
44
44
- bool refined_string_typet::is_c_string_type (const typet &type)
45
+ bool refined_string_typet::is_refined_string_type (const typet &type)
45
46
{
46
47
return
47
48
type.id ()==ID_struct &&
48
- to_struct_type (type).get_tag ()==CPROVER_PREFIX" string " ;
49
+ to_struct_type (type).get_tag ()==CPROVER_PREFIX" refined_string_type " ;
49
50
}
50
51
Original file line number Diff line number Diff line change @@ -42,10 +42,6 @@ class refined_string_typet: public struct_typet
42
42
return components ()[0 ].type ();
43
43
}
44
44
45
- // For C the unrefined string type is __CPROVER_string
46
-
47
- static bool is_c_string_type (const typet &type);
48
-
49
45
static bool is_refined_string_type (const typet &type);
50
46
51
47
constant_exprt index_of_int (int i) const
You can’t perform that action at this time.
0 commit comments