cprover
refined_string_type.cpp
Go to the documentation of this file.
1 /********************************************************************\
2 
3 Module: Type for string expressions used by the string solver.
4  These string expressions contain a field `length`, of type
5  `index_type`, a field `content` of type `content_type`.
6  This module also defines functions to recognise the C and java
7  string types.
8 
9 Author: Romain Brenguier, romain.brenguier@diffblue.com
10 
11 \*******************************************************************/
12 
18 
19 #include "refined_string_type.h"
20 
21 #include <util/cprover_prefix.h>
22 
24  const typet &index_type, const typet &char_type)
25 {
26  infinity_exprt infinite_index(index_type);
27  array_typet char_array(char_type, infinite_index);
28  components().emplace_back("length", index_type);
29  components().emplace_back("content", char_array);
30 }
31 
35 {
36  return
37  type.id()==ID_struct &&
38  to_struct_type(type).get_tag()==CPROVER_PREFIX"string";
39 }
40 
44 {
45  if(type.id()==ID_pointer)
46  {
47  const pointer_typet &pt=to_pointer_type(type);
48  const typet &subtype=pt.subtype();
50  }
51  return false;
52 }
53 
57 {
58  if(type.id()==ID_symbol)
59  {
61  return tag=="java::java.lang.String";
62  }
63  else if(type.id()==ID_struct)
64  {
65  irep_idt tag=to_struct_type(type).get_tag();
66  return tag=="java.lang.String";
67  }
68  return false;
69 }
70 
74 {
75  if(type.id()==ID_pointer)
76  {
77  const pointer_typet &pt=to_pointer_type(type);
78  const typet &subtype=pt.subtype();
79  if(subtype.id()==ID_struct)
80  {
82  return tag=="java.lang.StringBuilder";
83  }
84  }
85  return false;
86 }
87 
91 {
92  if(type.id()==ID_pointer)
93  {
94  const pointer_typet &pt=to_pointer_type(type);
95  const typet &subtype=pt.subtype();
96  if(subtype.id()==ID_struct)
97  {
98  const irep_idt &tag=to_struct_type(subtype).get_tag();
99  return tag=="java.lang.CharSequence";
100  }
101  }
102  return false;
103 }
The type of an expression.
Definition: type.h:20
static bool is_java_string_pointer_type(const typet &type)
#define CPROVER_PREFIX
static bool is_java_string_builder_type(const typet &type)
Type for string expressions used by the string solver.
static bool is_java_char_sequence_type(const typet &type)
static bool is_c_string_type(const typet &type)
const componentst & components() const
Definition: std_types.h:242
const irep_idt & id() const
Definition: irep.h:189
static bool is_java_string_type(const typet &type)
An expression denoting infinity.
Definition: std_expr.h:3908
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
The pointer type.
Definition: std_types.h:1343
bitvector_typet index_type()
Definition: c_types.cpp:15
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
arrays with given size
Definition: std_types.h:901
const typet & subtype() const
Definition: type.h:31
irep_idt get_tag() const
Definition: std_types.h:263
refined_string_typet(const typet &index_type, const typet &char_type)
bitvector_typet char_type()
Definition: c_types.cpp:113
const irep_idt & get_identifier() const
Definition: std_types.h:126