[WIP PATCH] Add why3 and frama-c

DoneSubmitted by Julien Lepiller.
Details
2 participants
  • Brett Gilio
  • Julien Lepiller
Owner
unassigned
Severity
normal
J
J
Julien Lepiller wrote on 16 Dec 2019 12:46
(address . guix-patches@gnu.org)
20191216124626.048f0e43@sybil.lepiller.eu
Hi Guix!
Since there was some interest very recently, I took another look at myincomplete why3 and frama-c packages. I updated them and polished thema 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 surehow these tools are supposed to be working.
Note that I didn't include ide support in why3 because this adds ~1GiBto the closure of the program. A good thing could be to separate thewhy3 library (not required when using why3) from the main package, in aseparate output.
For some reason, frama-c doesn't work directly, it needs to be in anenvironment 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 loadmodule 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 errormessage was emitted during execution. See above messages for moreinformation. [kernel] Frama-C aborted: invalid user input.
From 9fc13943b29196763524ddbc247218398d889459 Mon Sep 17 00:00:00 2001From: Julien Lepiller <julien@lepiller.eu>Date: Mon, 16 Dec 2019 12:09:16 +0100Subject: [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(-)
Toggle diff (112 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 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 2001From: Julien Lepiller <julien@lepiller.eu>Date: Mon, 16 Dec 2019 12:40:18 +0100Subject: [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(+)
Toggle diff (51 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 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
B
B
Brett Gilio wrote on 25 Dec 2019 08:01
(name . Julien Lepiller)(address . julien@lepiller.eu)
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 havebeen rather busy and have inadvertently put them off and forget theyexisted. Woops! My apologies.
I have Cc'ed Amin Bandali as we are both co-proposers for the formalmethods working group. These type checking and safety systems areobviously very important to the formal methods community and softwaredevelopers unaware of the nice guarantees offered by them. So i'd liketo 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 letyou know what I find. :)
-- Brett M. GilioGNU Guix, Contributor | GNU Project, Webmaster[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]<brettg@gnu.org> <brettg@posteo.net>
J
J
Julien Lepiller wrote on 2 Sep 2020 15:05
[WIP PATCH v2] Add why3 and frama-c
(address . 38635@debbugs.gnu.org)
20200902150508.5c4a45e8@tachikoma.lepiller.eu
Hi Guix!
I've updated my patches to the newest versions of why3 and frama-c. Theissue 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 loadplug-in 'frama-c-wp': cannot load module Details: error loading sharedlibrary: 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: Deferrederror message was emitted during execution. See above messages for moreinformation. [kernel] Frama-C aborted: invalid user input.
From 45254e8c70eb186a587c49295555e6c3096d67ab Mon Sep 17 00:00:00 2001From: Julien Lepiller <julien@lepiller.eu>Date: Mon, 16 Dec 2019 12:09:16 +0100Subject: [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(-)
Toggle diff (110 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 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 2001From: Julien Lepiller <julien@lepiller.eu>Date: Mon, 16 Dec 2019 12:40:18 +0100Subject: [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(+)
Toggle diff (48 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 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
J
J
Julien Lepiller wrote on 29 Apr 22:39 +0200
Re: [bug#38635] [PATCH v3] Add why3 and frama-c
(address . 38635@debbugs.gnu.org)
20210429223850.7659957a@tachikoma.lepiller.eu
Hi Guix!
I updated my patches to the latest version of frama-c, and the issue isgone now! Frama-c is working, as long as ocaml is in the environment(because it's calling ocaml-findlib that needs an environment variabledefined by the ocaml package).
From 103afc0730fda2b27a103bc66f1ff283b7883e8b Mon Sep 17 00:00:00 2001From: Julien Lepiller <julien@lepiller.eu>Date: Mon, 16 Dec 2019 12:09:16 +0100Subject: [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(-)
Toggle diff (102 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 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 2001From: Julien Lepiller <julien@lepiller.eu>Date: Mon, 16 Dec 2019 12:40:18 +0100Subject: [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(+)
Toggle diff (57 lines)diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scmindex 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
J
J
Julien Lepiller wrote on 2 Jun 03:11 +0200
(address . 38635-done@debbugs.gnu.org)
20210602031145.17815d14@tachikoma.lepiller.eu
After more than a month without a reply, I pushed to master asc9b3627d566bde6b60841185f147589df45e65eb andb94bc3ea30a9451f9019cca66ac20f585870eecd. Thanks!
Closed
?
Your comment

Commenting via the web interface is currently disabled.

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