File tree Expand file tree Collapse file tree 2 files changed +5
-8
lines changed Expand file tree Collapse file tree 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(
2929 array_typet char_array (char_type, infinite_index);
3030 components ().emplace_back (" length" , index_type);
3131 components ().emplace_back (" content" , char_array);
32+ set_tag (CPROVER_PREFIX" refined_string_type" );
3233}
3334
3435/* ******************************************************************\
3536
36- Function: refined_string_typet::is_c_string_type
37+ Function: refined_string_typet::is_refined_string_type
3738
3839 Inputs: a type
3940
40- Outputs: Boolean telling whether the type is that of C strings
41+ Outputs: Boolean telling whether the input is a refined string type
4142
4243\*******************************************************************/
4344
44- bool refined_string_typet::is_c_string_type (const typet &type)
45+ bool refined_string_typet::is_refined_string_type (const typet &type)
4546{
4647 return
4748 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 " ;
4950}
5051
Original file line number Diff line number Diff line change @@ -42,10 +42,6 @@ class refined_string_typet: public struct_typet
4242 return components ()[0 ].type ();
4343 }
4444
45- // For C the unrefined string type is __CPROVER_string
46-
47- static bool is_c_string_type (const typet &type);
48-
4945 static bool is_refined_string_type (const typet &type);
5046
5147 constant_exprt index_of_int (int i) const
You can’t perform that action at this time.
0 commit comments