Difference in output of --enum-range-check in goto-instrument and cbmc

[gsingh93]

CBMC version: 5.43.0
Operating system: Debian
Exact command line resulting in the issue: ~/cbmc/build/bin/cbmc out.gb --function bar
What behaviour did you expect: No violations
What happened instead: One violation

From other issues I've filed on here, I'm finding that while goto-instrument and cbmc share many options, the behavior between them sometimes differs. Can we document these differences on the website?

In this particular case, this is the problematic code:

typedef enum {
  SUCCESS,
  FAILURE,
} Foo;

Foo foo() {
  return SUCCESS;
}

void bar() {
  Foo f = foo();
}

The following works as expected, and all checks pass:

$ cbmc test.c --function bar --enum-range-check
...
** Results:
/path/to/test.c function bar
[bar.enum-range-check.1] line 11 enum range check in foo#return_value: SUCCESS
[bar.enum-range-check.2] line 11 enum range check in return_value_foo: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL

However, if I add the check with goto-instrument, I see a violation reported:

$ goto-cc test.c -o test.gb
$ goto-instrument --enum-range-check test.gb test-instrumented.gb
$ cbmc test-instrumented.gb --function bar
...
** Results:
/path/to/test.c function bar
[bar.enum-range-check.1] line 11 enum range check in return_value_foo: FAILURE
[bar.enum-range-check.2] line 11 enum range check in return_value_foo: SUCCESS

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

Any thoughts on why this is happening? Is there a general recommendation about where I should add any check? Should I always add them in the cbmc call or are there times where it's beneficial to add them to the goto-instrument call?

[tautschnig]

With apologies for taking this long to respond: more recent versions of CBMC will also yield this (spurious!) verification failure, because CBMC no longer performs return-value removal (as of 80fe6ff). The bug will be fixed once #6594 is merged.

[tautschnig]

Closing as #6594 has been merged.