Make string primitives return return_code_type

This could potentially be used to signal exceptions.

For primitives whose result is a string given as first parameter, the
returned value should have an integer type has given by get_return_code_type().

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -93,6 +93,12 @@ class string_constraint_generatort final
 
   exprt get_length_of_string_array(const array_string_exprt &s) const;
 
+  // Type used by primitives to signal errors
+  const signedbv_typet get_return_code_type()
+  {
+    return signedbv_typet(32);
+  }
+
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
   array_string_exprt

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -63,7 +63,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point(
     equal_exprt(res[1], typecast_exprt(second_char, char_type)));
   m_axioms.push_back(a5);
 
-  return res;
+  return from_integer(0, get_return_code_type());
 }
 
 /// the output is true when the character is a high surrogate for UTF-16

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -93,7 +93,7 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   m_axioms.push_back(a3);
 
   // We should have a enum type for the possible error codes
-  return from_integer(0, return_code_type);
+  return from_integer(0, get_return_code_type());
 }
 
 /// Add axioms to say that `res` is equal to the concatenation of `s1` and `s2`.

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -48,7 +48,7 @@ exprt string_constraint_generatort::add_axioms_for_constant(
   const exprt s_length = from_integer(str.size(), index_type);
 
   m_axioms.push_back(res.axiom_for_has_length(s_length));
-  return from_integer(0, signedbv_typet(32));
+  return from_integer(0, get_return_code_type());
 }
 
 /// add axioms to say that the returned string expression is empty
@@ -60,7 +60,7 @@ exprt string_constraint_generatort::add_axioms_for_empty_string(
   PRECONDITION(f.arguments().size() == 2);
   exprt length = f.arguments()[0];
   m_axioms.push_back(equal_exprt(length, from_integer(0, length.type())));
-  return from_integer(0, length.type());
+  return from_integer(0, get_return_code_type());
 }
 
 /// add axioms to say that the returned string expression is equal to the string

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -28,10 +28,13 @@ Author: Romain Brenguier, [email protected]
 #include <util/ssa_expr.h>
 
 string_constraint_generatort::string_constraint_generatort(
-  const string_constraint_generatort::infot& info, const namespacet& ns):
-  max_string_length(info.string_max_length),
-  m_force_printable_characters(info.string_printable),
-  m_ns(ns) { }
+  const string_constraint_generatort::infot &info,
+  const namespacet &ns)
+  : max_string_length(info.string_max_length),
+    m_force_printable_characters(info.string_printable),
+    m_ns(ns)
+{
+}
 
 const std::vector<exprt> &string_constraint_generatort::get_axioms() const
 {

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -244,7 +244,7 @@ exprt string_constraint_generatort::add_axioms_from_int_hex(
       m_axioms.push_back(
         implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
   }
-  return res;
+  return from_integer(0, get_return_code_type());
 }
 
 /// add axioms corresponding to the Integer.toHexString(I) java function
@@ -282,7 +282,7 @@ exprt string_constraint_generatort::add_axioms_from_char(
 {
   and_exprt lemma(equal_exprt(res[0], c), res.axiom_for_has_length(1));
   m_axioms.push_back(lemma);
-  return from_integer(0, signedbv_typet(32));
+  return from_integer(0, get_return_code_type());
 }
 
 /// Add axioms making the return value true if the given string is a correct