Since any use of the variable is undefined behavior, that's what we want to be informed about.
The reasoning about nondeterministic values should be spared for situations when it's other than undefined behavior. For instance, accessing an uninitialized structure member that came from malloc isn't undefined behavior. It's (I think) unspecified behavior. In an implementation that has trap representations for some types, it could hit a trap.
That's understandable, and I would suggest reaching out to the CBMC developers. It shouldn't be difficult to add an uninitialized variable pass to the solver.
Practically speaking, -Wall -Werror should catch this. Any use of a tool like CBMC should be part of a defense in depth strategy for code safety.
It does in clang.
$ cc -Wall -Werror bar.c
bar.c:5:11: error: variable 'x' is uninitialized when used here [-Werror,-Wuninitialized]
if (x <= 42){
^
bar.c:4:12: note: initialize the variable 'x' to silence this warning
int x;
^
= 0
$ cc --version
clang version 16.0.6
It also does in gcc.
$ gcc -Wall -Werror bar.c
bar.c: In function 'main':
bar.c:5:10: error: 'x' is used uninitialized [-Werror=uninitialized]
5 | if (x <= 42){
| ^
bar.c:4:11: note: 'x' was declared here
4 | int x;
| ^
cc1: all warnings being treated as errors
$ gcc --version
gcc 12.2.0
I do that! Some of my projects are packaged in distros. In the past, I've found discussions of problems among distro people, who didn't contact upstream at all, but just tried to patch things on their own. I fixed things on my end, and in such a way that their patch would fail to apply when they update. No words exchanged at all.
I'm not a user of CMBC. I read about it here, I wrote a comment here, and that's the end of it.
But for a minute I will bite. The submission has no link to the actual project. I found that by a web search.
The project has no project trappings: no mailing list, or anything of the sort. The page says, "For questions about CBMC, contact Daniel Kroening". The name is a link to his home page. His home page has no obvious contact information. There are links to papers; probably his e-mail address is given in some of them. Let's click on "A Tool for Checking ANSI-C Programs". Hey, e-mail links in that page, before we even get to the PDF. But ... from 2004. Is k-----g@cs.cmu.edu from two decades ago going to work, given that he's at Oxford?
Suppose I hunt down his current e-mail address. What do I say? "Dear Sir, I feel really awkward to be contacting you about your CBMC program, which I have never actually used, but believe me when I say I have a valuable suggestion ..."
If I used the thing, I'd fix it myself and send a patch!
https://github.com/diffblue/cbmc The github repo is active and they are very responsive to issues. As you say, it is unneccesary and probably undesirable to post an issue for a tool you don't use. The links for this are multiple places in the submission. The state of the cprover website is unfortunate and represents the state of the project unfairly imo.
FWIW I have had luck mailing old research emails, I read my 20 year old university email. It is one of the best signal to noise ratios in communications I have.
I would not mail if it is only about unintialized variables.
When I say that a variable is used, I mean that its value is accessed. This is in line with compiler jargon. In this basic block, the variable x has no next use at the first line; the assignment of 42 is a dead assignment.
The reasoning about nondeterministic values should be spared for situations when it's other than undefined behavior. For instance, accessing an uninitialized structure member that came from malloc isn't undefined behavior. It's (I think) unspecified behavior. In an implementation that has trap representations for some types, it could hit a trap.