diff mbox series

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

Message ID 20210429223850.7659957a@tachikoma.lepiller.eu
State Accepted
Headers show
Series [bug#38635,v3] Add why3 and frama-c | expand

Checks

Context Check Description
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue

Commit Message

Julien Lepiller April 29, 2021, 8:39 p.m. UTC 
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).

Comments

Julien Lepiller June 2, 2021, 1:11 a.m. UTC | #1 
After more than a month without a reply, I pushed to master as
c9b3627d566bde6b60841185f147589df45e65eb and
b94bc3ea30a9451f9019cca66ac20f585870eecd. Thanks!
diff mbox series

Patch

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