| Message ID | 20191216124626.048f0e43@sybil.lepiller.eu |
|---|---|
| State | Work in progress |
| Headers | show |
| Series | [bug#38635,WIP] Add why3 and frama-c | expand |
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. :)
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