cprover
string_constraint_generator_insert.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for the family of insert Java functions
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
19  const string_exprt &s1, const string_exprt &s2, const exprt &offset)
20 {
21  assert(offset.type()==s1.length().type());
23  s1, from_integer(0, offset.type()), offset);
24  string_exprt suf=add_axioms_for_substring(s1, offset, s1.length());
25  string_exprt concat1=add_axioms_for_concat(pref, s2);
26  return add_axioms_for_concat(concat1, suf);
27 }
28 
35 {
38  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
39 }
40 
48 {
52  args(f, 3)[2], MAX_INTEGER_LENGTH, ref_type);
53  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
54 }
55 
63 {
67  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
68 }
69 
77 {
80  string_exprt s2=add_axioms_from_bool(args(f, 3)[2], ref_type);
81  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
82 }
83 
91 {
93  const refined_string_typet &ref_type=to_refined_string_type(s1.type());
94  string_exprt s2=add_axioms_from_char(args(f, 3)[2], ref_type);
95  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
96 }
97 
105 {
108  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
109 }
110 
118 {
121  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
122 }
123 
133 {
134  exprt offset;
135  exprt count;
136  if(f.arguments().size()==6)
137  {
138  offset=f.arguments()[4];
139  count=f.arguments()[5];
140  }
141  else
142  {
143  assert(f.arguments().size()==4);
144  count=f.arguments()[2];
145  offset=from_integer(0, count.type());
146  }
147 
149  const exprt &length=f.arguments()[2];
150  const exprt &data=f.arguments()[3];
152  length, data, offset, count);
153  return add_axioms_for_insert(str, arr, f.arguments()[1]);
154 }
string_exprt add_axioms_for_insert_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(C) java function
string_exprt add_axioms_for_insert_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(I) java function
Generates string constraints to link results from string functions with their arguments.
application of (mathematical) function
Definition: std_expr.h:3785
string_exprt add_axioms_from_bool(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(Z) java function
string_exprt add_axioms_for_insert_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(F) java function
argumentst & arguments()
Definition: std_expr.h:3805
string_exprt add_axioms_for_insert_long(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(J) java function
typet & type()
Definition: expr.h:60
string_exprt add_axioms_for_insert_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(D) java function
const exprt & length() const
Definition: string_expr.h:35
string_exprt add_axioms_from_float(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(F) java function
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
string_exprt add_axioms_for_insert_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(Z) java function
string_exprt add_axioms_for_concat(const string_exprt &s1, const string_exprt &s2)
add axioms to say that the returned string expression is equal to the concatenation of the two string...
string_exprt add_axioms_for_insert(const string_exprt &s1, const string_exprt &s2, const exprt &offset)
add axioms stating that the result correspond to the first string where we inserted the second one at...
string_exprt add_axioms_from_char(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(C) java function
Base class for all expressions.
Definition: expr.h:46
string_exprt add_axioms_from_int(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(I) java function
int8_t s1
Definition: bytecode_info.h:59
int16_t s2
Definition: bytecode_info.h:60
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
string_exprt add_axioms_for_insert_char_array(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert:(I[CII) and StringBuilder.insert:(I[C) java func...
Definition: kdev_t.h:24
string_exprt add_axioms_from_char_array(const function_application_exprt &f)
add axioms corresponding to the String.
string_exprt add_axioms_for_substring(const string_exprt &str, const exprt &start, const exprt &end)
add axioms stating that the returned string expression is equal to the input one starting at start an...