cprover
string_refinement_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String solver
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
10 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
11 
12 #include <memory>
13 
15 #include "string_constraint.h"
17 
25 bool is_char_type(const typet &type);
26 
32 bool is_char_array_type(const typet &type, const namespacet &ns);
33 
37 bool is_char_pointer_type(const typet &type);
38 
45 bool has_char_pointer_subtype(const typet &type, const namespacet &ns);
46 
50 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
51 
57 std::string
58 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
59 
61 {
62  std::map<exprt, std::set<exprt>> cumulative;
63  std::map<exprt, std::set<exprt>> current;
64 };
65 
67 {
68  std::vector<string_constraintt> universal;
69  std::vector<string_not_contains_constraintt> not_contains;
70 };
71 
75 {
76 public:
81  explicit sparse_arrayt(const with_exprt &expr);
82 
85  static exprt to_if_expression(const with_exprt &expr, const exprt &index);
86 
87 protected:
89  std::map<std::size_t, exprt> entries;
91  {
92  }
93 };
94 
100 {
101 public:
106  explicit interval_sparse_arrayt(const with_exprt &expr) : sparse_arrayt(expr)
107  {
108  }
109 
113  interval_sparse_arrayt(const array_exprt &expr, const exprt &extra_value);
114 
119  const array_list_exprt &expr,
120  const exprt &extra_value);
121 
122  exprt to_if_expression(const exprt &index) const;
123 
127  of_expr(const exprt &expr, const exprt &extra_value);
128 
130  array_exprt concretize(std::size_t size, const typet &index_type) const;
131 
134  exprt at(std::size_t index) const;
135 
139  {
140  }
141 };
142 
143 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
bitvector_typet index_type()
Definition: c_types.cpp:16
Array constructor from list of elements.
Definition: std_expr.h:1382
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1428
Base class for all expressions.
Definition: expr.h:54
Represents arrays by the indexes up to which the value remains the same.
exprt to_if_expression(const exprt &index) const
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor,...
interval_sparse_arrayt(exprt default_value)
Array containing the same value at each index.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
interval_sparse_arrayt(const with_exprt &expr)
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for ...
exprt at(std::size_t index) const
Get the value at the specified index.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
std::map< std::size_t, exprt > entries
sparse_arrayt(exprt default_value)
static exprt to_if_expression(const with_exprt &expr, const exprt &index)
Creates an if_expr corresponding to the result of accessing the array at the given index.
sparse_arrayt(const with_exprt &expr)
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ....
The type of an expression, extends irept.
Definition: type.h:28
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
nonstd::optional< T > optionalt
Definition: optional.h:35
Defines string constraints.
Generates string constraints to link results from string functions with their arguments.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
std::map< exprt, std::set< exprt > > current
std::map< exprt, std::set< exprt > > cumulative
std::vector< string_constraintt > universal
std::vector< string_not_contains_constraintt > not_contains