4 ms·
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.
by nanolith 3y ago
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 3y ago> 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 3y agoYou'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 3y agoI 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!
- pastage 3y agoFWIW 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.
- philzook 3y agohttps://github.com/diffblue/cbmc 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.
- deleted 3y ago[deleted]
- deleted 3y ago[deleted]
- kazinator 3y agoI do not have an account on github and do not engage projects that have selected github as their only means of interaction.
- mort96 3y agoPeople can comment on a project in public discussion forums without then also having a responsibility to become a contributor to the project.
- akoboldfrying 3y agoI 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."