From c4ad3f73033c7e0511c3e7df961e1232cc503478 Mon Sep 17 00:00:00 2001 From: Thomas Schwinge Date: Wed, 26 Feb 2014 12:32:06 +0100 Subject: IRC. --- open_issues/code_analysis.mdwn | 66 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 64 insertions(+), 2 deletions(-) (limited to 'open_issues/code_analysis.mdwn') diff --git a/open_issues/code_analysis.mdwn b/open_issues/code_analysis.mdwn index 67798c6a..d61d5921 100644 --- a/open_issues/code_analysis.mdwn +++ b/open_issues/code_analysis.mdwn @@ -1,5 +1,5 @@ -[[!meta copyright="Copyright © 2010, 2011, 2012, 2013 Free Software Foundation, -Inc."]] +[[!meta copyright="Copyright © 2010, 2011, 2012, 2013, 2014 Free Software +Foundation, Inc."]] [[!meta license="""[[!toggle id="license" text="GFDL 1.2+"]][[!toggleable id="license" text="Permission is granted to copy, distribute and/or modify this @@ -87,8 +87,70 @@ There is a [[!FF_project 276]][[!tag bounty]] on some of these tasks. * [Frama-C](http://frama-c.com/) + btw, I've been looking at http://frama-c.com/ lately + it's a theorem prover for c/c++ + oh nice + I think it's most impressive, it works on the hurd (aptitude + install frama-c o_O) + *and it works + "Simple things should be simple, + complex things should be possible." + :) + looks great + even the gui is awesome, allows one to browse source code in + a very impressive way + clear separation between value changes, dependencies, side + effects + we could have plugins for stuff like ports + handles concurrency oO + so you want to use Frame-C to analyze the whole Hurd code + base? + nalaginrut: well, frama-c looks "able" to assist in + analyzing the Hurd, yes + nalaginrut: but theorem proving is a manual process, one + needs to guide the prover + nalaginrut: b/c some stuff is not decideable + 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 + that's not a problem + each server can be analyzed separately + braunr: also, each "entry point" + alright, but sounds a big work + it is + otherwise, formal verification would be widespread :) + that, and most tools are horrible to use, frama-c is really + an exception in this regard + * [Coverity](http://www.coverity.com/) (nonfree?) + * IRC, OFTC, #debian-hurd, 2014-02-03 + + btw, did you consider adding hurd and mach to to detect bugs automatically? + I found lots of bugs in gnash, ipmitool and sysvinit when I + started scanning those projects. :) + i did some static analysis work, i haven't used coverty + but free tools for that + i think thomas wanted to look into coverty though + quite easy to set up, but you need to download and run a + non-free tarball on the build host. + does that tar ball contains binary code ? + that'd be a show stopper for the hurd of course + did not investigate. I just put it in a contained virtual + machine. + did not want it on my laptop. :) + prefer free software here. :) + but I did not have to "accept license", at least. :) + + * IRC, OFTC, #debian-hurd, 2014-02-05 + + ah, cool. + is now in place. :) + + [[microkernel/mach/gnumach/projects/clean_up_the_code]], + *Code_Analysis, Coverity*. + * [Splint](http://www.splint.org/) * IRC, freenode, #hurd, 2011-12-04 -- cgit v1.2.3