`--nondet-static-exclude` silently fails

CBMC version: 5.95.1 Operating system: N/A

Considering the following C program.

int foo = 0;

int f() {
    static int bar = 0;
    return bar;
}

int main() {
    assert(foo == 0);
    assert(f() == 0);
    return;
}

First, we compile using goto-cc.

goto-cc main.c -o main.goto

If we want to instrument the code using --nondet-static-exclude to preserve the value of bar, we can instrument the binary as follows:

goto-instrument main.goto main-ins.goto --nondet-static-exclude bar

This will produce an error message.

Condition: !not_found
Reason: we are assuming that a name exists in the namespace when this function is called - identifier bar was not found
Backtrace:

The documentation of --nondet-static-exclude doesn't specify any restrictions on its inputs.

--nondet-static-exclude e    same as nondet-static except for the variable e (use multiple times if required)

If we observe the symbol table, we can try to use the symbol name, which I thought it'd be the most reliable option.

Symbol......: f::1::bar
Pretty name.: f::1::bar
Module......: main
Base name...: bar
Mode........: C
Type........: signed int
Value.......: 0
Flags.......: lvalue static_lifetime file_local
Location....: file main.c line 4 function f

However, goto-instrument silently fails.

Reading GOTO program from 'main.goto'
Adding nondeterministic initialization of static/global variables except for the specified ones.
Writing GOTO program to 'main-ins.goto'

If we observe the GOTO program, we can see that bar is non-deterministically initialized along with foo.

        // 18 file main.c line 4 function f
        ASSIGN f::1::bar := side_effect statement="nondet" is_nondet_nullable="1"
        // 19 file main.c line 1
        ASSIGN foo := side_effect statement="nondet" is_nondet_nullable="1"

After a few attempts with no error messages, only using the path and the pretty name we can finally get the expected behavior.

goto-instrument main.goto main-ins.goto --nondet-static-exclude main.c:f::1::bar

One may say the pretty name and the symbol name are the same, but this is not always the case. In my attempts, using the symbol name and the path does not work either. If we now inspect the GOTO program, we can confirm the effect of the instrumentation and verification proceeds as expected.

        ASSIGN f::1::bar := 0
        // 19 file main.c line 1
        ASSIGN foo := side_effect statement="nondet" is_nondet_nullable="1"

What was the expected behavior? I'd expect that CBMC will report an error message whenever it can't exclude variable e from the pool of variables that will be non-deterministically initialized. I also expected that using only the symbol name would be sufficient (and reliable).

diffblue / cbmc

`--nondet-static-exclude` silently fails #8225