cprover
refined_string_type.h
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 #ifndef CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H
20 #define CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H
21 
22 #include <util/std_types.h>
23 #include <util/std_expr.h>
24 #include <util/arith_tools.h>
25 #include <util/expr_util.h>
26 
27 // Internal type used for string refinement
29 {
30 public:
32 
33  // Type for the content (list of characters) of a string
35  {
36  assert(components().size()==2);
37  return to_array_type(components()[1].type());
38  }
39 
40  const typet &get_char_type() const
41  {
42  assert(components().size()==2);
43  return components()[0].type();
44  }
45 
46  const typet &get_index_type() const
47  {
48  return get_content_type().size().type();
49  }
50 
51  // For C the unrefined string type is __CPROVER_string, for java it is a
52  // pointer to a struct with tag java.lang.String
53 
54  static bool is_c_string_type(const typet &type);
55 
56  static bool is_java_string_pointer_type(const typet &type);
57 
58  static bool is_java_string_type(const typet &type);
59 
60  static bool is_java_string_builder_type(const typet &type);
61 
62  static bool is_java_char_sequence_type(const typet &type);
63 
64  static bool is_unrefined_string_type(const typet &type)
65  {
66  return (
67  is_c_string_type(type) ||
71  }
72 
73  static bool is_unrefined_string(const exprt &expr)
74  {
75  return (is_unrefined_string_type(expr.type()));
76  }
77 
79  {
80  return from_integer(i, get_index_type());
81  }
82 };
83 
85 {
86  assert(type.id()==ID_struct);
87  return static_cast<const refined_string_typet &>(type);
88 }
89 
90 #endif
The type of an expression.
Definition: type.h:20
static bool is_java_string_pointer_type(const typet &type)
const typet & get_char_type() const
static bool is_java_string_builder_type(const typet &type)
Deprecated expression utility functions.
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
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
const array_typet & get_content_type() const
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
static bool is_java_string_type(const typet &type)
static bool is_unrefined_string_type(const typet &type)
const refined_string_typet & to_refined_string_type(const typet &type)
API to expression classes.
static bool is_unrefined_string(const exprt &expr)
const exprt & size() const
Definition: std_types.h:915
const typet & get_index_type() const
bitvector_typet index_type()
Definition: c_types.cpp:15
API to type classes.
Base class for all expressions.
Definition: expr.h:46
constant_exprt index_of_int(int i) const
arrays with given size
Definition: std_types.h:901
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
refined_string_typet(const typet &index_type, const typet &char_type)
bitvector_typet char_type()
Definition: c_types.cpp:113