From 66092474535401ff36d18a6f2ad77c45dcb2b9ae Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Mar 2018 17:52:09 +0000
Subject: [PATCH] Add a maybe_testing_function to builtin functions

This is to know whether the result of a function can be used outside of
string operations.
---
 .../refinement/string_builtin_function.h      | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 55ada98f353..282810c6775 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -40,6 +40,14 @@ class string_builtin_functiont
 
   exprt return_code;
 
+  /// Tells whether the builtin function can be a testing function, that is a
+  /// function that does not return a string, for instance like `equals`,
+  /// `indexOf` or `compare`.
+  virtual bool maybe_testing_function() const
+  {
+    return true;
+  }
+
 private:
   string_builtin_functiont() = default;
 
@@ -84,6 +92,11 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
 
   optionalt<exprt>
   eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  bool maybe_testing_function() const override
+  {
+    return false;
+  }
 };
 
 /// Adding a character at the end of a string
@@ -170,6 +183,11 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
     UNREACHABLE;
   };
 
+  bool maybe_testing_function() const override
+  {
+    return false;
+  }
+
 protected:
   explicit string_insertion_builtin_functiont(const exprt &return_code)
     : string_builtin_functiont(return_code)
@@ -225,6 +243,11 @@ class string_creation_builtin_functiont : public string_builtin_functiont
   {
     return result;
   }
+
+  bool maybe_testing_function() const override
+  {
+    return false;
+  }
 };
 
 /// String test