[WIP PATCH] Add why3 and frama-c

Julien Lepiller wrote on 16 Dec 2019 12:46

Recipients:(address . guix-patches@gnu.org)

Message-ID:20191216124626.048f0e43@sybil.lepiller.eu

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.

From 9fc13943b29196763524ddbc247218398d889459 Mon Sep 17 00:00:00 2001

* gnu/packages/maths.scm (why3): New variable.

---

gnu/packages/maths.scm | 67 +++++++++++++++++++++++++++++++++++++++++-

1 file changed, 66 insertions(+), 1 deletion(-)

Toggle diff (112 lines)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

From f9501f1cc5725d49c69c948f6f7cc70c13f1dbdc Mon Sep 17 00:00:00 2001

* gnu/packages/maths.scm (frama-c): New variable.

---

gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++

1 file changed, 38 insertions(+)

Toggle diff (51 lines)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

Brett Gilio wrote on 25 Dec 2019 08:01

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)

Message-ID:878sn0zy57.fsf@gnu.org

Julien Lepiller <julien@lepiller.eu> writes:

Toggle quote (36 lines)> 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>

Julien Lepiller wrote on 2 Sep 2020 15:05

[WIP PATCH v2] Add why3 and frama-c

Recipients:(address . 38635@debbugs.gnu.org)

Message-ID:20200902150508.5c4a45e8@tachikoma.lepiller.eu

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.

From 45254e8c70eb186a587c49295555e6c3096d67ab Mon Sep 17 00:00:00 2001

* gnu/packages/maths.scm (why3): New variable.

---

gnu/packages/maths.scm | 67 +++++++++++++++++++++++++++++++++++++++++-

1 file changed, 66 insertions(+), 1 deletion(-)

Toggle diff (110 lines)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

From 408f2a6feffc8d86d0e3ff31b891614b160ed142 Mon Sep 17 00:00:00 2001

* gnu/packages/maths.scm (frama-c): New variable.

---

gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++

1 file changed, 38 insertions(+)

Toggle diff (48 lines)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

Julien Lepiller wrote on 29 Apr 2021 22:39

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

Recipients:(address . 38635@debbugs.gnu.org)

Message-ID:20210429223850.7659957a@tachikoma.lepiller.eu

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).

From 103afc0730fda2b27a103bc66f1ff283b7883e8b Mon Sep 17 00:00:00 2001

* gnu/packages/maths.scm (why3): New variable.

---

gnu/packages/maths.scm | 66 +++++++++++++++++++++++++++++++++++++++++-

1 file changed, 65 insertions(+), 1 deletion(-)

Toggle diff (102 lines)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

From 431dc3f0212c53b60f075e4e2719531f2ad4d84a Mon Sep 17 00:00:00 2001

* gnu/packages/maths.scm (frama-c): New variable.

---

gnu/packages/maths.scm | 47 ++++++++++++++++++++++++++++++++++++++++++

1 file changed, 47 insertions(+)

Toggle diff (57 lines)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

Julien Lepiller wrote on 2 Jun 2021 03:11

Recipients:(address . 38635-done@debbugs.gnu.org)

Message-ID:20210602031145.17815d14@tachikoma.lepiller.eu

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

Closed

Your comment

This issue is archived.

To comment on this conversation send email to 38635@debbugs.gnu.org

is:open	open issues
is:done	closed issues
submitter:<who>	search issue submitter
author:<who>	search by message author
date:yesterday..now	search by issue date
mdate:3m..2d	search by message date