From 408f2a6feffc8d86d0e3ff31b891614b160ed142 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(+)
@@ -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