__CPROVER_enum_is_in_range() fails on enum value returning functions.

[ilvn]

CBMC version: 5.48.0 (cbmc-5.48.0)
Operating system: macOS 12.1 (21C52)
Exact command line resulting in the issue: cbmc --enum-range-check x.c
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead: VERIFICATION FAILED

This is the test code

// x.c

enum enm { first, second, third, fourth, };

static enum enm efunc(void)
{
    return second;
}

int main(void)
{
    enum enm e = efunc();
    __CPROVER_assert(__CPROVER_enum_is_in_range(e), "enum failure");
    return (e);
}

The verification result when verified with cbmc --enum-range-check x.c

** Results:
x.c function main
[main.enum-range-check.1] line 12 enum range check in return_value_efunc: FAILURE
[main.enum-range-check.2] line 12 enum range check in return_value_efunc: SUCCESS
[main.assertion.1] line 13 enum failure: SUCCESS
[main.enum-range-check.3] line 13 enum range check in e: SUCCESS
[main.enum-range-check.4] line 13 enum range check in e: SUCCESS
[main.enum-range-check.5] line 13 enum range check in e: SUCCESS
[main.enum-range-check.6] line 13 enum range check in e: SUCCESS
[main.enum-range-check.7] line 14 enum range check in e: SUCCESS

** 1 of 8 failed (2 iterations)
VERIFICATION FAILED

The verification reports failure in line 12 enum enm e = efunc();.
Replacing function call with e.g. enum enm e = second; will give successful verification, as expected.

[tautschnig]

Thank you for your report! It seems that we wrongly insert this check multiple times, where one of these insertions is before even making an assignment to the value. (Note how lines 12 and 13 appear multiple times in the output.)

[tautschnig]

Thank you again for your detailed report. This will be fixed once #6594 has been merged.

[ilvn]

Great! Thank you for the fix.