IRC.

1 files changed, 64 insertions, 2 deletions

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/)
 
+        <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](http://www.coverity.com/) (nonfree?)
 
+      * 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. :)
+
+        [[microkernel/mach/gnumach/projects/clean_up_the_code]],
+        *Code_Analysis, Coverity*.
+
   * [Splint](http://www.splint.org/)
 
       * IRC, freenode, #hurd, 2011-12-04