__CPROVER_enum_is_in_range should not yield redundant assertions

The assertions generated by --enum-range-check must not apply to
the expansion of __CPROVER_enum_is_in_range, for those would assert
exactly the same. Also, those expressions are rather costly: for N enum
values, N assertions would be generated.

Author: tautschnig

regression/cbmc/enum_is_in_range/no_duplicate.desc

@@ -5,4 +5,7 @@ no_duplicate.c
 ^EXIT=0$
 ^SIGNAL=0$
 --
+line 17 enum range check in e: SUCCESS$
 --
+Test that enum range checks aren't applied to function-call left-hand sides, and
+that no extra checks are generated for uses of __CPROVER_enum_is_in_range.

src/goto-programs/builtin_functions.cpp

@@ -634,6 +634,7 @@ void goto_convertt::do_enum_is_in_range(
 
   code_assignt assignment(lhs, disjunction(disjuncts));
   assignment.add_source_location() = function.source_location();
+  assignment.add_source_location().add_pragma("disable:enum-range-check");
   copy(assignment, ASSIGN, dest);
 }