Skip to content

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

@gsingh93

Description

@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?

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions