GNU Hurd/ open issues/ code analysis

Welcome to... ... the GNU Hurd!

In the topic of code analysis or program analysis (Wikipedia article), there is static code analysis (Wikipedia article) and dynamic program analysis (Wikipedia article). This topic overlaps with performance analysis, formal verification, as well as general debugging.

  1. Bounty
  2. Static
  3. Dynamic

Bounty

There is a FOSS Factory bounty (p276) on some of these tasks.

Static

  • GCC's warnings. Yes, really.

    • GCC plugins can be used for additional semantic analysis. For example, http://lwn.net/Articles/457543/, and search for kernel context in the comments.

    • Have GCC make use of RPC/MIG in/out specifiers, and have it emit useful warnings in case these are pointing to uninitialized data (for in only).

  • List of tools for static code analysis

  • Engineering zero-defect software, Eric S. Raymond, 2012-05-13

  • Static Source Code Analysis Tools for C

  • Cppcheck

    For example, Debian's hurd_20110319-2 package (Samuel Thibault, 2011-08-05: I had a look at those, some are spurious; the realloc issues are for real).

  • Coccinelle

    Has already been used for finding and fixing double mutex unlocking issues.

  • clang

  • Linux' sparse

  • http://klee.llvm.org/

  • Smatch

  • Parfait

  • Saturn

  • Flawfinder

  • sixgill

  • s-spider

  • CIL (C Intermediate Language)

  • Frama-C

    <teythoon> btw, I've been looking at http://frama-c.com/ lately
<teythoon> it's a theorem prover for c/c++
<braunr> oh nice
<teythoon> I think it's most impressive, it works on the hurd (aptitude
  install frama-c o_O)
<teythoon> *and it works
<braunr> "Simple things should be simple,
<braunr> complex things should be possible."
<braunr> :)
<braunr> looks great
<teythoon> even the gui is awesome, allows one to browse source code in
  a very impressive way
<braunr> clear separation between value changes, dependencies, side
  effects
<braunr> we could have plugins for stuff like ports
<braunr> handles concurrency oO
<nalaginrut> so you want to use Frame-C to analyze the whole Hurd code
  base?
<teythoon> nalaginrut: well, frama-c looks "able" to assist in
  analyzing the Hurd, yes
<teythoon> nalaginrut: but theorem proving is a manual process, one
  needs to guide the prover
<teythoon> nalaginrut: b/c some stuff is not decideable
<nalaginrut> I ask this because I can imagine how to analyze Linux
  since all the code is in a directory. But Hurd's codes are
  distributed to many other projects
<braunr> that's not a problem
<braunr> each server can be analyzed separately
<teythoon> braunr: also, each "entry point"
<nalaginrut> alright, but sounds a big work
<teythoon> it is
<braunr> otherwise, formal verification would be widespread :)
<teythoon> that, and most tools are horrible to use, frama-c is really
  an exception in this regard

  • Coverity (nonfree)

    • https://scan.coverity.com/projects/1307 If you want access, speak up in #hurd or on the mailing list.

    • IRC, OFTC, #debian-hurd, 2014-02-03

      <pere> btw, did you consider adding hurd and mach to <URL:
  https://scan.coverity.com/ > to detect bugs automatically?
<pere> I found lots of bugs in gnash, ipmitool and sysvinit when I
  started scanning those projects. :)
<teythoon> i did some static analysis work, i haven't used coverty
  but free tools for that
<teythoon> i think thomas wanted to look into coverty though
<pere> quite easy to set up, but you need to download and run a
  non-free tarball on the build host.
<teythoon> does that tar ball contains binary code ?
<teythoon> that'd be a show stopper for the hurd of course
<pere> did not investigate.  I just put it in a contained virtual
  machine.
<pere> did not want it on my laptop. :)
<pere> prefer free software here. :)
<pere> but I did not have to "accept license", at least. :)

    • IRC, OFTC, #debian-hurd, 2014-02-05

      <pere> ah, cool.  <URL: https://scan.coverity.com/projects/1307 >
  is now in place. :)

      clean up the code, Code_Analysis, Coverity.

  • Splint

    • IRC, freenode, #hurd, 2011-12-04

      <mcsim> has anyone used splint on hurd?
<mcsim> this is tool for statically checking C programs
<mcsim> seems I made it work

Hurd-specific Applications

Dynamic