Move disjunction construction to goto conversion

This moves the construction of the disjunction that does
the actual enum_is_in_range checks into the goto conversion
part of the code (and correctly removes it from the
type checking).

Author: TGWDB

src/ansi-c/c_typecheck_expr.cpp

@@ -2852,28 +2852,9 @@ exprt c_typecheck_baset::do_special_functions(
                     << expr.arguments().size() << " were provided";
       throw invalid_source_file_exceptiont{error_message.str()};
     }
-    // Replace expr with giant boolean that checks all the values
-    // of the enumeration as disjunction
-    // This code is similar to goto_checkt::enum_range_check
     auto arg1 = expr.arguments()[0];
     typecheck_expr(arg1);
-    if(
-      auto c_enum_tag_type =
-        type_try_dynamic_cast<c_enum_tag_typet>(arg1.type()))
-    {
-      const c_enum_typet &c_enum_type = follow_tag(*c_enum_tag_type);
-      const c_enum_typet::memberst enum_values = c_enum_type.members();
-
-      std::vector<exprt> disjuncts;
-      for(const auto &enum_value : enum_values)
-      {
-        constant_exprt val{enum_value.get_value(), *c_enum_tag_type};
-        disjuncts.push_back(equal_exprt(arg1, std::move(val)));
-      }
-
-      return disjunction(disjuncts);
-    }
-    else
+    if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
     {
       // Can't enum range check a non-enum
       std::ostringstream error_message;
@@ -2882,6 +2863,10 @@ exprt c_typecheck_baset::do_special_functions(
                     << ") has type `" << type2c(arg1.type(), *this) << '`';
       throw invalid_source_file_exceptiont{error_message.str()};
     }
+    else
+    {
+      return expr;
+    }
   }
   else if(
     identifier == "__builtin_add_overflow" ||

src/goto-programs/builtin_functions.cpp

@@ -610,6 +610,34 @@ exprt make_va_list(const exprt &expr)
   return result;
 }
 
+void goto_convertt::do_enum_is_in_range(
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments,
+  goto_programt &dest)
+{
+  PRECONDITION(arguments.size() == 1);
+  const auto enum_expr = arguments.front();
+  const auto enum_type =
+    type_try_dynamic_cast<c_enum_tag_typet>(enum_expr.type());
+  PRECONDITION(enum_type);
+  const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type);
+  const c_enum_typet::memberst enum_values = c_enum_type.members();
+
+  std::vector<exprt> disjuncts;
+  for(const auto &enum_value : enum_values)
+  {
+    constant_exprt val{enum_value.get_value(), *enum_type};
+    disjuncts.push_back(equal_exprt(enum_expr, std::move(val)));
+  }
+
+  const auto disjunction = ::disjunction(disjuncts);
+
+  code_assignt assignment(lhs, disjunction);
+  assignment.add_source_location() = function.source_location();
+  copy(assignment, ASSIGN, dest);
+}
+
 /// add function calls to function queue for later processing
 void goto_convertt::do_function_call_symbol(
   const exprt &lhs,
@@ -734,6 +762,10 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
   }
+  else if(identifier == CPROVER_PREFIX "enum_is_in_range")
+  {
+    do_enum_is_in_range(lhs, function, arguments, dest);
+  }
   else if(
     identifier == CPROVER_PREFIX "assert" ||
     identifier == CPROVER_PREFIX "precondition" ||

src/goto-programs/goto_convert_class.h

@@ -589,6 +589,11 @@ class goto_convertt:public messaget
   exprt get_constant(const exprt &expr);
 
   // some built-in functions
+  void do_enum_is_in_range(
+    const exprt &lhs,
+    const symbol_exprt &function,
+    const exprt::operandst &arguments,
+    goto_programt &dest);
   void do_atomic_begin(
     const exprt &lhs,
     const symbol_exprt &function,