[bug#38635] [WIP PATCH] Add why3 and frama-c

[bug#38635] [WIP PATCH] Add why3 and frama-c

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 1648 bytes --]

Hi Guix!

Since there was some interest very recently, I took another look at my
incomplete why3 and frama-c packages. I updated them and polished them
a little. I encourage formal-method guixers to test these patches,
especially if you are a user of why3 or frama-c, because I'm not sure
how these tools are supposed to be working.

Note that I didn't include ide support in why3 because this adds ~1GiB
to the closure of the program. A good thing could be to separate the
why3 library (not required when using why3) from the main package, in a
separate output.

For some reason, frama-c doesn't work directly, it needs to be in an
environment where its dependencies are present, hence the propagation.
However, it's failing at runtime:

$ guix environment --ad-hoc frama-c ocaml ocaml-findlib
[env]$ frama-c --help

[kernel] User Error: cannot load plug-in 'zip': cannot load
module Details: error loading shared library:
/gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/zip/zip.cmxa:
invalid ELF header [kernel] User Error: cannot load plug-in 'why3':
cannot load module Details: error loading shared library:
/gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/why3/why3.cmxs:
undefined symbol: camlGzip [kernel] User Error: cannot load plug-in
'frama-c-wp': cannot load module Details: error loading shared library:
/gnu/store/daqn9vsc15j3slbalw2fag6amndv8x98-frama-c-20.0/lib/frama-c/plugins/top/Wp.cmxs:
undefined symbol: camlWhy3__Theory [kernel] User Error: Deferred error
message was emitted during execution. See above messages for more
information. [kernel] Frama-C aborted: invalid user input.

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0001-gnu-Add-why3.patch --]
[-- Type: text/x-patch, Size: 4884 bytes --]

From 9fc13943b29196763524ddbc247218398d889459 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 16 Dec 2019 12:09:16 +0100
Subject: [PATCH 1/2] gnu: Add why3.

* gnu/packages/maths.scm (why3): New variable.
---
 gnu/packages/maths.scm | 67 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 0ed61ad4a1..991f164737 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -28,7 +28,7 @@
 ;;; Copyright © 2018 Adam Massmann <massmannak@gmail.com>
 ;;; Copyright © 2018 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
-;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018, 2019 Julien Lepiller <julien@lepiller.eu>
 ;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;; Copyright © 2019 Nicolas Goaziou <mail@nicolasgoaziou.fr>
 ;;; Copyright © 2019 Steve Sprang <scs@stevesprang.com>
@@ -61,6 +61,7 @@
   #:use-module ((guix build utils) #:select (alist-replace))
   #:use-module (guix build-system cmake)
   #:use-module (guix build-system gnu)
+  #:use-module (guix build-system ocaml)
   #:use-module (guix build-system python)
   #:use-module (guix build-system ruby)
   #:use-module (gnu packages algebra)
@@ -72,10 +73,12 @@
   #:use-module (gnu packages check)
   #:use-module (gnu packages cmake)
   #:use-module (gnu packages compression)
+  #:use-module (gnu packages coq)
   #:use-module (gnu packages curl)
   #:use-module (gnu packages cyrus-sasl)
   #:use-module (gnu packages documentation)
   #:use-module (gnu packages elf)
+  #:use-module (gnu packages emacs)
   #:use-module (gnu packages flex)
   #:use-module (gnu packages fltk)
   #:use-module (gnu packages fontutils)
@@ -101,6 +104,7 @@
   #:use-module (gnu packages mpi)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages netpbm)
+  #:use-module (gnu packages ocaml)
   #:use-module (gnu packages onc-rpc)
   #:use-module (gnu packages pcre)
   #:use-module (gnu packages popt)
@@ -4182,6 +4186,67 @@ as equations, scalars, vectors, and matrices.")
 theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
     (license license:expat)))
 
+(define-public why3
+  (package
+    (name "why3")
+    (version "1.2.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/file"
+                                  "/38185/why3-" version ".tar.gz"))
+              (sha256
+               (base32
+                "014gkwisjp05x3342zxkryb729p02ngx1hcjjsrplpa53jzgz647"))))
+    (build-system ocaml-build-system)
+    (native-inputs
+     `(("coq" ,coq)
+       ("ocaml" ,ocaml)
+       ("which" ,which)))
+    (propagated-inputs
+     `(("camlzip" ,camlzip)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-menhir" ,ocaml-menhir)
+       ("ocaml-num" ,ocaml-num)
+       ("ocaml-zarith" ,ocaml-zarith)))
+    (inputs
+     `(("coq-flocq" ,coq-flocq)
+       ("emacs-minimal" ,emacs-minimal)
+       ("zlib" ,zlib)))
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-configure
+           (lambda _
+             (setenv "CONFIG_SHELL" (which "sh"))
+             (substitute* "configure"
+               ;; find ocaml-num in the correct directory
+               (("\\$DIR/nums.cma") "$DIR/../nums.cma")
+               (("\\$DIR/num.cmi") "$DIR/../num.cmi"))
+             #t))
+         (add-after 'configure 'fix-makefile
+           (lambda _
+             (substitute* "Makefile"
+               ;; find ocaml-num in the correct directory
+               (("site-lib/num") "site-lib"))
+             #t))
+	 (add-after 'install 'install-lib
+	   (lambda _
+	     (invoke "make" "byte")
+	     (invoke "make" "install-lib")
+	     #t)))))
+    (home-page "http://why3.lri.fr")
+    (synopsis "Deductive program verification")
+    (description "Why3 provides a language for specification and programming,
+called WhyML, and relies on external theorem provers, both automated and
+interactive, to discharge verification conditions.  Why3 comes with a standard
+library of logical theories (integer and real arithmetic, Boolean operations,
+sets and maps, etc.) and basic programming data structures (arrays, queues,
+hash tables, etc.).  A user can write WhyML programs directly and get
+correct-by-construction OCaml programs through an automated extraction
+mechanism.  WhyML is also used as an intermediate language for the verification
+of C, Java, or Ada programs.")
+    (license license:lgpl2.1)))
+
 (define-public elpa
   (package
     (name "elpa")
-- 
2.24.0


[-- Attachment #3: 0002-gnu-Add-frama-c.patch --]
[-- Type: text/x-patch, Size: 2267 bytes --]

From f9501f1cc5725d49c69c948f6f7cc70c13f1dbdc Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 16 Dec 2019 12:40:18 +0100
Subject: [PATCH 2/2] gnu: Add frama-c.

* gnu/packages/maths.scm (frama-c): New variable.
---
 gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 991f164737..d4e3e74c98 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -4247,6 +4247,44 @@ mechanism.  WhyML is also used as an intermediate language for the verification
 of C, Java, or Ada programs.")
     (license license:lgpl2.1)))
 
+(define-public frama-c
+  (package
+    (name "frama-c")
+    (version "20.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://frama-c.com/download/frama-c-"
+                                  version "-Calcium.tar.gz"))
+              (sha256
+               (base32
+                "03dvn162djylj2skmk6vv75gh87mm4s5cspkzcrlm5x0rlla2yqn"))))
+    (build-system ocaml-build-system)
+    (arguments
+     `(#:tests? #f; no test target in Makefile
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'export-shell
+           (lambda* (#:key inputs #:allow-other-keys)
+             (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash")
+                                                   "/bin/sh"))
+             #t)))))
+    (inputs
+     `(("gmp" ,gmp)))
+    (propagated-inputs
+     `(("ocaml-biniou" ,ocaml-biniou)
+       ("ocaml-easy-format" ,ocaml-easy-format)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-yojson" ,ocaml-yojson)
+       ("ocaml-zarith" ,ocaml-zarith)
+       ("why3" ,why3)))
+    (home-page "http://frama-c.com")
+    (synopsis "C source code analysis platform")
+    (description "Frama-C is an extensible and collaborative platform dedicated
+to source-code analysis of C software.  The Frama-C analyzers assist you in
+various source-code-related activities, from the navigation through unfamiliar
+projects up to the certification of critical software.")
+    (license license:lgpl2.1+)))
+
 (define-public elpa
   (package
     (name "elpa")
-- 
2.24.0

[bug#38635] [WIP PATCH] Add why3 and frama-c

[Brett Gilio]

Julien Lepiller <julien@lepiller.eu> writes:

> Hi Guix!
>
> Since there was some interest very recently, I took another look at my
> incomplete why3 and frama-c packages. I updated them and polished them
> a little. I encourage formal-method guixers to test these patches,
> especially if you are a user of why3 or frama-c, because I'm not sure
> how these tools are supposed to be working.
>
> Note that I didn't include ide support in why3 because this adds ~1GiB
> to the closure of the program. A good thing could be to separate the
> why3 library (not required when using why3) from the main package, in a
> separate output.
>
> For some reason, frama-c doesn't work directly, it needs to be in an
> environment where its dependencies are present, hence the propagation.
> However, it's failing at runtime:
>
> $ guix environment --ad-hoc frama-c ocaml ocaml-findlib
> [env]$ frama-c --help
>
> [kernel] User Error: cannot load plug-in 'zip': cannot load
> module Details: error loading shared library:
> /gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/zip/zip.cmxa:
> invalid ELF header [kernel] User Error: cannot load plug-in 'why3':
> cannot load module Details: error loading shared library:
> /gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/why3/why3.cmxs:
> undefined symbol: camlGzip [kernel] User Error: cannot load plug-in
> 'frama-c-wp': cannot load module Details: error loading shared library:
> /gnu/store/daqn9vsc15j3slbalw2fag6amndv8x98-frama-c-20.0/lib/frama-c/plugins/top/Wp.cmxs:
> undefined symbol: camlWhy3__Theory [kernel] User Error: Deferred error
> message was emitted during execution. See above messages for more
> information. [kernel] Frama-C aborted: invalid user input.
>
>
>

Hey Julien,

Sorry for the delay. I got your patches the day you sent them, but have
been rather busy and have inadvertently put them off and forget they
existed. Woops! My apologies.

I have Cc'ed Amin Bandali as we are both co-proposers for the formal
methods working group. These type checking and safety systems are
obviously very important to the formal methods community and software
developers unaware of the nice guarantees offered by them. So i'd like
to see this get added and in shape regardless of if the Guix maintainers
"approve" our working group proposal.

Thank you for sharing this. I will take another look at it soon and let
you know what I find. :)

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>

[bug#38635] [WIP PATCH v2] Add why3 and frama-c

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 1132 bytes --]

Hi Guix!

I've updated my patches to the newest versions of why3 and frama-c. The
issue is still present as before:

$ frama-c --help

[kernel] User Error: cannot load plug-in 'zip': cannot load module
  Details: error loading shared library: Dynlink.Error
(Dynlink.Cannot_open_dll
"Failure(\"/gnu/store/jrbkl0ls1vqnr1w7gcbg8jlxcd1jp71m-profile/lib/ocaml/site-lib/zip/zip.cmxa:
invalid ELF header\")") [kernel] User Error: cannot load plug-in
'why3': cannot load module Details: error loading shared library:
Dynlink.Error (Dynlink.Cannot_open_dll
"Failure(\"/gnu/store/jrbkl0ls1vqnr1w7gcbg8jlxcd1jp71m-profile/lib/ocaml/site-lib/why3/why3.cmxs:
undefined symbol: camlGzip\")") [kernel] User Error: cannot load
plug-in 'frama-c-wp': cannot load module Details: error loading shared
library: Dynlink.Error (Dynlink.Cannot_open_dll
"Failure(\"/gnu/store/bicyz7li6bvrxh4kh2h1dc5398bx5xsm-frama-c-21.1/lib/frama-c/plugins/top/Wp.cmxs:
undefined symbol: camlWhy3__Theory\")") [kernel] User Error: Deferred
error message was emitted during execution. See above messages for more
information. [kernel] Frama-C aborted: invalid user input.

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0001-gnu-Add-why3.patch --]
[-- Type: text/x-patch, Size: 4927 bytes --]

From 45254e8c70eb186a587c49295555e6c3096d67ab Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 16 Dec 2019 12:09:16 +0100
Subject: [PATCH 1/2] gnu: Add why3.

* gnu/packages/maths.scm (why3): New variable.
---
 gnu/packages/maths.scm | 67 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 97f57ddd24..aa3d0da77c 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -28,7 +28,7 @@
 ;;; Copyright © 2018 Adam Massmann <massmannak@gmail.com>
 ;;; Copyright © 2018, 2020 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
-;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018-2020 Julien Lepiller <julien@lepiller.eu>
 ;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;; Copyright © 2019 Nicolas Goaziou <mail@nicolasgoaziou.fr>
 ;;; Copyright © 2019 Steve Sprang <scs@stevesprang.com>
@@ -69,6 +69,7 @@
   #:use-module (guix build-system cmake)
   #:use-module (guix build-system glib-or-gtk)
   #:use-module (guix build-system gnu)
+  #:use-module (guix build-system ocaml)
   #:use-module (guix build-system python)
   #:use-module (guix build-system ruby)
   #:use-module (gnu packages algebra)
@@ -80,11 +81,13 @@
   #:use-module (gnu packages check)
   #:use-module (gnu packages cmake)
   #:use-module (gnu packages compression)
+  #:use-module (gnu packages coq)
   #:use-module (gnu packages curl)
   #:use-module (gnu packages cyrus-sasl)
   #:use-module (gnu packages dbm)
   #:use-module (gnu packages documentation)
   #:use-module (gnu packages elf)
+  #:use-module (gnu packages emacs)
   #:use-module (gnu packages file)
   #:use-module (gnu packages flex)
   #:use-module (gnu packages fltk)
@@ -113,6 +116,7 @@
   #:use-module (gnu packages mpi)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages netpbm)
+  #:use-module (gnu packages ocaml)
   #:use-module (gnu packages onc-rpc)
   #:use-module (gnu packages pcre)
   #:use-module (gnu packages popt)
@@ -5970,3 +5974,64 @@ and conversions, physical constants, symbolic calculations (including
 integrals and equations), arbitrary precision, uncertainty propagation,
 interval arithmetic, plotting.")
     (license license:gpl2+)))
+
+(define-public why3
+  (package
+    (name "why3")
+    (version "1.3.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/file"
+                                  "/38291/why3-" version ".tar.gz"))
+              (sha256
+               (base32
+                "16zcrc60zz2j3gd3ww93z2z9x2jkxb3kr57y8i5rcgmacy7mw3bv"))))
+    (build-system ocaml-build-system)
+    (native-inputs
+     `(("coq" ,coq)
+       ("ocaml" ,ocaml)
+       ("which" ,which)))
+    (propagated-inputs
+     `(("camlzip" ,camlzip)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-menhir" ,ocaml-menhir)
+       ("ocaml-num" ,ocaml-num)
+       ("ocaml-zarith" ,ocaml-zarith)))
+    (inputs
+     `(("coq-flocq" ,coq-flocq)
+       ("emacs-minimal" ,emacs-minimal)
+       ("zlib" ,zlib)))
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-configure
+           (lambda _
+             (setenv "CONFIG_SHELL" (which "sh"))
+             (substitute* "configure"
+               ;; find ocaml-num in the correct directory
+               (("\\$DIR/nums.cma") "$DIR/../nums.cma")
+               (("\\$DIR/num.cmi") "$DIR/../num.cmi"))
+             #t))
+         (add-after 'configure 'fix-makefile
+           (lambda _
+             (substitute* "Makefile"
+               ;; find ocaml-num in the correct directory
+               (("site-lib/num") "site-lib"))
+             #t))
+        (add-after 'install 'install-lib
+          (lambda _
+            (invoke "make" "byte")
+            (invoke "make" "install-lib")
+            #t)))))
+    (home-page "http://why3.lri.fr")
+    (synopsis "Deductive program verification")
+    (description "Why3 provides a language for specification and programming,
+called WhyML, and relies on external theorem provers, both automated and
+interactive, to discharge verification conditions.  Why3 comes with a standard
+library of logical theories (integer and real arithmetic, Boolean operations,
+sets and maps, etc.) and basic programming data structures (arrays, queues,
+hash tables, etc.).  A user can write WhyML programs directly and get
+correct-by-construction OCaml programs through an automated extraction
+mechanism.  WhyML is also used as an intermediate language for the verification
+of C, Java, or Ada programs.")
+    (license license:lgpl2.1)))
-- 
2.28.0


[-- Attachment #3: 0002-gnu-Add-frama-c.patch --]
[-- Type: text/x-patch, Size: 2286 bytes --]

From 408f2a6feffc8d86d0e3ff31b891614b160ed142 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 16 Dec 2019 12:40:18 +0100
Subject: [PATCH 2/2] gnu: Add frama-c.

* gnu/packages/maths.scm (frama-c): New variable.
---
 gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index aa3d0da77c..a18d35504c 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -6035,3 +6035,41 @@ correct-by-construction OCaml programs through an automated extraction
 mechanism.  WhyML is also used as an intermediate language for the verification
 of C, Java, or Ada programs.")
     (license license:lgpl2.1)))
+
+(define-public frama-c
+  (package
+    (name "frama-c")
+    (version "21.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://frama-c.com/download/frama-c-"
+                                  version "-Scandium.tar.gz"))
+              (sha256
+               (base32
+                "0qq0d08dzr0dmdjysiimdqmwlzgnn932vp5kf8lfn3nl45ai09dy"))))
+    (build-system ocaml-build-system)
+    (arguments
+     `(#:tests? #f; no test target in Makefile
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'export-shell
+           (lambda* (#:key inputs #:allow-other-keys)
+             (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash")
+                                                   "/bin/sh"))
+             #t)))))
+    (inputs
+     `(("gmp" ,gmp)))
+    (propagated-inputs
+     `(("ocaml-biniou" ,ocaml-biniou)
+       ("ocaml-easy-format" ,ocaml-easy-format)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-yojson" ,ocaml-yojson)
+       ("ocaml-zarith" ,ocaml-zarith)
+       ("why3" ,why3)))
+    (home-page "http://frama-c.com")
+    (synopsis "C source code analysis platform")
+    (description "Frama-C is an extensible and collaborative platform dedicated
+to source-code analysis of C software.  The Frama-C analyzers assist you in
+various source-code-related activities, from the navigation through unfamiliar
+projects up to the certification of critical software.")
+    (license license:lgpl2.1+)))
-- 
2.28.0

[bug#38635] [PATCH v3] Add why3 and frama-c

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 253 bytes --]

Hi Guix!

I updated my patches to the latest version of frama-c, and the issue is
gone now! Frama-c is working, as long as ocaml is in the environment
(because it's calling ocaml-findlib that needs an environment variable
defined by the ocaml package).

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0001-gnu-Add-why3.patch --]
[-- Type: text/x-patch, Size: 4639 bytes --]

From 103afc0730fda2b27a103bc66f1ff283b7883e8b Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 16 Dec 2019 12:09:16 +0100
Subject: [PATCH 1/2] gnu: Add why3.

* gnu/packages/maths.scm (why3): New variable.
---
 gnu/packages/maths.scm | 66 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 65 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index a79e128955..a214b5d780 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -28,7 +28,7 @@
 ;;; Copyright © 2018 Adam Massmann <massmannak@gmail.com>
 ;;; Copyright © 2018, 2020 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
-;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018, 2021 Julien Lepiller <julien@lepiller.eu>
 ;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;; Copyright © 2019, 2021 Nicolas Goaziou <mail@nicolasgoaziou.fr>
 ;;; Copyright © 2019 Steve Sprang <scs@stevesprang.com>
@@ -74,6 +74,7 @@
   #:use-module (guix build-system cmake)
   #:use-module (guix build-system glib-or-gtk)
   #:use-module (guix build-system gnu)
+  #:use-module (guix build-system ocaml)
   #:use-module (guix build-system python)
   #:use-module (guix build-system ruby)
   #:use-module (gnu packages algebra)
@@ -85,11 +86,13 @@
   #:use-module (gnu packages check)
   #:use-module (gnu packages cmake)
   #:use-module (gnu packages compression)
+  #:use-module (gnu packages coq)
   #:use-module (gnu packages curl)
   #:use-module (gnu packages cyrus-sasl)
   #:use-module (gnu packages dbm)
   #:use-module (gnu packages documentation)
   #:use-module (gnu packages elf)
+  #:use-module (gnu packages emacs)
   #:use-module (gnu packages file)
   #:use-module (gnu packages flex)
   #:use-module (gnu packages fltk)
@@ -6190,3 +6193,64 @@ and conversions, physical constants, symbolic calculations (including
 integrals and equations), arbitrary precision, uncertainty propagation,
 interval arithmetic, plotting.")
     (license license:gpl2+)))
+
+(define-public why3
+  (package
+    (name "why3")
+    (version "1.3.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/file"
+                                  "/38291/why3-" version ".tar.gz"))
+              (sha256
+               (base32
+                "16zcrc60zz2j3gd3ww93z2z9x2jkxb3kr57y8i5rcgmacy7mw3bv"))))
+    (build-system ocaml-build-system)
+    (native-inputs
+     `(("coq" ,coq)
+       ("ocaml" ,ocaml)
+       ("which" ,which)))
+    (propagated-inputs
+     `(("camlzip" ,camlzip)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-menhir" ,ocaml-menhir)
+       ("ocaml-num" ,ocaml-num)
+       ("ocaml-zarith" ,ocaml-zarith)))
+    (inputs
+     `(("coq-flocq" ,coq-flocq)
+       ("emacs-minimal" ,emacs-minimal)
+       ("zlib" ,zlib)))
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-configure
+           (lambda _
+             (setenv "CONFIG_SHELL" (which "sh"))
+             (substitute* "configure"
+               ;; find ocaml-num in the correct directory
+               (("\\$DIR/nums.cma") "$DIR/../nums.cma")
+               (("\\$DIR/num.cmi") "$DIR/../num.cmi"))
+             #t))
+         (add-after 'configure 'fix-makefile
+           (lambda _
+             (substitute* "Makefile"
+               ;; find ocaml-num in the correct directory
+               (("site-lib/num") "site-lib"))
+             #t))
+        (add-after 'install 'install-lib
+          (lambda _
+            (invoke "make" "byte")
+            (invoke "make" "install-lib")
+            #t)))))
+    (home-page "http://why3.lri.fr")
+    (synopsis "Deductive program verification")
+    (description "Why3 provides a language for specification and programming,
+called WhyML, and relies on external theorem provers, both automated and
+interactive, to discharge verification conditions.  Why3 comes with a standard
+library of logical theories (integer and real arithmetic, Boolean operations,
+sets and maps, etc.) and basic programming data structures (arrays, queues,
+hash tables, etc.).  A user can write WhyML programs directly and get
+correct-by-construction OCaml programs through an automated extraction
+mechanism.  WhyML is also used as an intermediate language for the verification
+of C, Java, or Ada programs.")
+    (license license:lgpl2.1)))
-- 
2.26.3


[-- Attachment #3: 0002-gnu-Add-frama-c.patch --]
[-- Type: text/x-patch, Size: 2608 bytes --]

From 431dc3f0212c53b60f075e4e2719531f2ad4d84a Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 16 Dec 2019 12:40:18 +0100
Subject: [PATCH 2/2] gnu: Add frama-c.

* gnu/packages/maths.scm (frama-c): New variable.
---
 gnu/packages/maths.scm | 47 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index a214b5d780..49a3fd3904 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -6254,3 +6254,50 @@ correct-by-construction OCaml programs through an automated extraction
 mechanism.  WhyML is also used as an intermediate language for the verification
 of C, Java, or Ada programs.")
     (license license:lgpl2.1)))
+
+(define-public frama-c
+  (package
+    (name "frama-c")
+    (version "22.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://frama-c.com/download/frama-c-"
+                                  version "-Titanium.tar.gz"))
+              (sha256
+               (base32
+                "1mq1fijka95ydrla486yr4w6wdl9l7vmp512s1q00b0p6lmfwmkh"))))
+    (build-system ocaml-build-system)
+    (arguments
+     `(#:tests? #f; no test target in Makefile
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'export-shell
+           (lambda* (#:key inputs #:allow-other-keys)
+             (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash")
+                                                   "/bin/sh"))
+             #t)))))
+    (inputs
+     `(("gmp" ,gmp)))
+    (propagated-inputs
+     `(("ocaml-biniou" ,ocaml-biniou)
+       ("ocaml-easy-format" ,ocaml-easy-format)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-yojson" ,ocaml-yojson)
+       ("ocaml-zarith" ,ocaml-zarith)
+       ("why3" ,why3)))
+    (native-search-paths
+     (list (search-path-specification
+            (variable "FRAMAC_SHARE")
+            (files '("share/frama-c"))
+            (separator #f))
+           (search-path-specification
+            (variable "FRAMAC_LIB")
+            (files '("lib/frama-c"))
+            (separator #f))))
+    (home-page "http://frama-c.com")
+    (synopsis "C source code analysis platform")
+    (description "Frama-C is an extensible and collaborative platform dedicated
+to source-code analysis of C software.  The Frama-C analyzers assist you in
+various source-code-related activities, from the navigation through unfamiliar
+projects up to the certification of critical software.")
+    (license license:lgpl2.1+)))
-- 
2.26.3

bug#38635: [PATCH v3] Add why3 and frama-c

[Julien Lepiller]

After more than a month without a reply, I pushed to master as
c9b3627d566bde6b60841185f147589df45e65eb and
b94bc3ea30a9451f9019cca66ac20f585870eecd. Thanks!