LWN: Comments on "Finding kernel problems automatically"

I can complain ...

arafel — 2004-07-16T15:37:39+00:00

I sent a couple of notes, and got replies saying that they'd release it when they'd tidied the code up. Doesn't look like that's going to happen.

Regarding the other bit - they'll port the checker code to whichever compiler you want. If it's gcc, then I can't see that they have any way of stopping you from redistributing it afterwards - but you'd have to have enough money to pay for the port.

This makes me think...

dvdeug — 2004-06-04T10:38:48+00:00

Yes, witness C++. Part of C++'s problem is that it's an incredible pain to parse correctly (notice that GCC ended up completely rewritting the C++ parser to properly support standard C++.) Part of the reason is that C++ was designed based on the already complex C syntax.

Another problem with C++ is that C--especially real world C, but even standard C--and C++ aren't completely compatible either way. Stroustroup had to make a few minor tweaks that lost compatibility to make C++ work right. A strong-C is more than likely going to have a few edge cases where things don't work exactly the same.

To use a few preprocessor defines to remove the strong-C is going to hamstring your efforts; the differences are just not going to be that minimal, and that tightly limits your syntax. What you're asking for is basically the system described in the article, not a new language.

This makes me think...

bronson — 2004-06-03T23:27:43+00:00

Except that, with a few preprocessor defines to remove the strong-C keywords, you could compile strong-C on a weak-C compiler. The kernel source code could even be a mix of strong and weak C as it transitions to strong-C over the period of a few years. There are very real benefits to simply extending an existing language -- witness C++.

I can complain ...

AnswerGuy — 2004-06-03T22:34:06+00:00

... that the Stanford Checker was built around gcc (xgcc) and thus should be obligated by the GPL if they ever distribute it.

So, if Coverity is selling (distributing) a derivative of this as a product ...

Now, it's possible that they took *their* code and ported it to some other compiler environment; or it's possible they are billing this as a service and not as a product.

However, it doesn't seem like they are acting in the spirit of free software in either case.

I can also complain since I sent them a number of messages politely asking for information about the project and it's progress and inquiring about the the possibility having anyone from their team speak at a local technical group (BayLISA) and never received the courtesy of a response --- not even a curt note to the effect that they are far to busy and important to speak to the likes of us sysadmins.

Oh well! C'est le vie!

JimD

This makes me think...

mmarsh — 2004-06-03T15:12:27+00:00

You might want to check out http://www.cs.cornell.edu/projects/cyclone/ ,
as well. It's certainly not a standard, but it's a safe C dialect.

This makes me think...

bdixon — 2004-06-03T11:34:57+00:00

Yes... It is called MISRA (Motor Industry Software Reliability Association) C and it amounts to many rules asking you to do this and not do that. MISRA C compliance can be checked using static analyzers. For example, rule 33 says that the right hand operand of && or || shall not contain side effects.

Some of the MISRA rules, however, may not be compatible with systems programming.

This makes me think...

dvdeug — 2004-06-03T10:47:49+00:00

Why would you want a version of C with strong-typing? It wouldn't be C anymore; it would probably be no easier to port code from C to new-C than it would to port it to Ada or some other real language with strong typing. If you want Ada, or Java, or Modula-3, or even C++, you know where to find them.

This makes me think...

etrusco — 2004-06-03T05:06:50+00:00

Has there ever been a tentative to push a "hardened C" standard, just C plus strong type-checking?