helper for getting the function type used in function_application_exprt

src/goto-symex/goto_symex.cpp

@@ -382,7 +382,7 @@ void goto_symext::constant_propagate_empty_string(
   symex_assignt &symex_assign,
   const function_application_exprt &f_l1)
 {
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -410,7 +410,7 @@ bool goto_symext::constant_propagate_string_concat(
   symex_assignt &symex_assign,
   const function_application_exprt &f_l1)
 {
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -465,7 +465,7 @@ bool goto_symext::constant_propagate_string_substring(
   PRECONDITION(num_operands >= 4);
   PRECONDITION(num_operands <= 5);
 
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -557,7 +557,7 @@ bool goto_symext::constant_propagate_integer_to_string(
   PRECONDITION(num_operands >= 3);
   PRECONDITION(num_operands <= 4);
 
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -633,7 +633,7 @@ bool goto_symext::constant_propagate_delete_char_at(
   // - index of char to delete
   PRECONDITION(f_l1.arguments().size() == 4);
 
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -707,7 +707,7 @@ bool goto_symext::constant_propagate_delete(
   // - index of end of substring to delete (exclusive)
   PRECONDITION(f_l1.arguments().size() == 5);
 
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -800,7 +800,7 @@ bool goto_symext::constant_propagate_set_length(
   // - new length of the string
   PRECONDITION(f_l1.arguments().size() == 4);
 
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -882,7 +882,7 @@ bool goto_symext::constant_propagate_set_char_at(
   // - new char
   PRECONDITION(f_l1.arguments().size() == 5);
 
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -945,7 +945,7 @@ bool goto_symext::constant_propagate_case_change(
   const function_application_exprt &f_l1,
   bool to_upper)
 {
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -1006,7 +1006,7 @@ bool goto_symext::constant_propagate_replace(
   symex_assignt &symex_assign,
   const function_application_exprt &f_l1)
 {
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 
@@ -1114,7 +1114,7 @@ bool goto_symext::constant_propagate_trim(
   symex_assignt &symex_assign,
   const function_application_exprt &f_l1)
 {
-  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
   const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
 

src/util/mathematical_expr.cpp

@@ -18,6 +18,12 @@ function_application_exprt::function_application_exprt(
       tuple_exprt(std::move(_arguments)),
       to_mathematical_function_type(_function.type()).codomain())
 {
-  const auto &domain = to_mathematical_function_type(_function.type()).domain();
+  const auto &domain = function_type().domain();
   PRECONDITION(domain.size() == arguments().size());
 }
+
+const mathematical_function_typet &
+function_application_exprt::function_type() const
+{
+  return to_mathematical_function_type(function().type());
+}

src/util/mathematical_expr.h

@@ -186,12 +186,16 @@ class tuple_exprt : public multi_ary_exprt
   }
 };
 
+class mathematical_function_typet;
+
 /// \brief Application of (mathematical) function
 class function_application_exprt : public binary_exprt
 {
 public:
   using argumentst = exprt::operandst;
 
+  /// \param _function must be known to have \ref mathematical_function_typet type.
+  /// \param _arguments must match function_type().domain()
   function_application_exprt(const exprt &_function, argumentst _arguments);
 
   exprt &function()
@@ -204,6 +208,9 @@ class function_application_exprt : public binary_exprt
     return op0();
   }
 
+  /// This helper method provides the type of the expression returned by \ref function.
+  const mathematical_function_typet &function_type() const;
+
   argumentst &arguments()
   {
     return op1().operands();