[bug#38635,WIP] Add why3 and frama-c
diff mbox series

Message ID 20191216124626.048f0e43@sybil.lepiller.eu
State New
Headers show
Series
  • [bug#38635,WIP] Add why3 and frama-c
Related show

Commit Message

Julien Lepiller Dec. 16, 2019, 11:46 a.m. UTC
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.

Comments

Brett Gilio Dec. 25, 2019, 7:01 a.m. UTC | #1
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. :)

Patch
diff mbox series

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