[kazinator]

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.

[nanolith]

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

[kazinator]

> I would suggest reaching out to the CBMC developers

For something I don't use?

How about this: I would suggest the CMBC developers read HN comments about their stuff, when it comes up.

[akoboldfrying]

You're right, notifying them directly would be too much effort.

The sensible way for developers to become aware of possible improvements they could make is for them to constantly scan the rest of the internet.

[kazinator]

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 [e-mail] 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!

[philzook]

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.

[kazinator]

I do not have an account on github and do not engage projects that have selected github as their only means of interaction.

[pastage]

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.

[mort96]

People can comment on a project in public discussion forums without then also having a responsibility to become a contributor to the project.

[akoboldfrying]

I certainly agree -- but then they should not expect anything to be done about whatever they're complaining about.

I interpreted kazinator's original comment as essentially saying "This looks like something I might use myself, but for this dealbreaker issue."

[fsckboy]

>Since any use of the variable is undefined behavior

use of the variable as an lvalue is not undefined

[kazinator]

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.

  x = 42
  y = w
  x = 43

Search the web for "next-use information".