frama-c: rename from framac, 31.0 -> 32.1
Co-authored-by: redianthus <l@ndrs.fr>
This commit is contained in:
Lucas Ransan
committed by
Lucas Ransan
Lucas Ransan
parent
b88623e40b
commit
13517922bd
@@ -0,0 +1,139 @@
|
||||
{
|
||||
lib,
|
||||
stdenv,
|
||||
darwin,
|
||||
fetchurl,
|
||||
graphviz,
|
||||
doxygen,
|
||||
ocamlPackages,
|
||||
coq,
|
||||
dune,
|
||||
why3,
|
||||
gdk-pixbuf,
|
||||
wrapGAppsHook3,
|
||||
withGui ? true,
|
||||
withWP ? true,
|
||||
withMarkdown ? true,
|
||||
withApron ? true,
|
||||
withZeroMQ ? true,
|
||||
}:
|
||||
|
||||
stdenv.mkDerivation (finalAttrs: {
|
||||
pname = "frama-c";
|
||||
version = "32.1";
|
||||
slang = "Germanium";
|
||||
|
||||
__structuredAttrs = true;
|
||||
|
||||
src = fetchurl {
|
||||
url = "https://frama-c.com/download/frama-c-${finalAttrs.version}-${finalAttrs.slang}.tar.gz";
|
||||
hash = "sha256-3V1uid9d3mpAs4vq0wLQpbmGCxw7ZbzYU2CneAh8E+I=";
|
||||
};
|
||||
|
||||
preConfigure = ''
|
||||
substituteInPlace src/dune --replace-fail " bytes " " "
|
||||
substituteInPlace Makefile --replace-fail "include ivette/Makefile.installation" ""
|
||||
'';
|
||||
|
||||
strictDeps = true;
|
||||
|
||||
nativeBuildInputs = [
|
||||
wrapGAppsHook3
|
||||
dune
|
||||
]
|
||||
++ (with ocamlPackages; [
|
||||
ocaml
|
||||
findlib
|
||||
menhir
|
||||
])
|
||||
++ lib.optionals stdenv.hostPlatform.isDarwin [
|
||||
darwin.sigtool
|
||||
];
|
||||
|
||||
buildInputs =
|
||||
with ocamlPackages;
|
||||
[
|
||||
camlzip
|
||||
dune-configurator
|
||||
dune-site
|
||||
menhirLib
|
||||
ocamlgraph
|
||||
ppx_deriving
|
||||
ppx_deriving_yaml
|
||||
ppx_inline_test
|
||||
unionFind
|
||||
yojson
|
||||
zarith
|
||||
]
|
||||
++ lib.optionals withGui [
|
||||
lablgtk3
|
||||
lablgtk3-sourceview3
|
||||
]
|
||||
++ lib.optionals withWP [
|
||||
why3
|
||||
]
|
||||
++ lib.optionals withMarkdown [
|
||||
ppx_deriving_yojson
|
||||
]
|
||||
++ lib.optionals withApron [
|
||||
apron
|
||||
]
|
||||
++ lib.optionals withZeroMQ [
|
||||
zmq
|
||||
];
|
||||
|
||||
buildPhase = ''
|
||||
runHook preBuild
|
||||
dune build ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} --release @install
|
||||
runHook postBuild
|
||||
'';
|
||||
|
||||
installFlags = [ "PREFIX=$(out)" ];
|
||||
|
||||
preFixup =
|
||||
let
|
||||
runtimeDeps =
|
||||
with ocamlPackages;
|
||||
finalAttrs.buildInputs
|
||||
++ [
|
||||
bigarray-compat
|
||||
mlgmpidl
|
||||
parsexp
|
||||
re
|
||||
seq
|
||||
sexplib
|
||||
]
|
||||
++ lib.optionals withWP [
|
||||
why3.dev
|
||||
]
|
||||
++ lib.optionals withApron [
|
||||
apron.dev
|
||||
];
|
||||
|
||||
ocamlPath = lib.makeSearchPath "/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib" runtimeDeps;
|
||||
in
|
||||
''
|
||||
gappsWrapperArgs+=(--prefix OCAMLPATH ':' ${ocamlPath}:$out/lib/)
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Extensible and collaborative platform dedicated to source-code analysis of C software";
|
||||
longDescription = ''
|
||||
Frama-C is an open-source 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.
|
||||
'';
|
||||
homepage = "https://www.frama-c.com/index.html";
|
||||
license = lib.licenses.lgpl21;
|
||||
maintainers = with lib.maintainers; [
|
||||
thoughtpolice
|
||||
amiddelk
|
||||
luc65r
|
||||
];
|
||||
platforms = lib.platforms.unix;
|
||||
mainProgram = "frama-c";
|
||||
broken = !lib.versionAtLeast ocamlPackages.ocaml.version "4.14";
|
||||
};
|
||||
})
|
||||
@@ -1,143 +0,0 @@
|
||||
{
|
||||
lib,
|
||||
stdenv,
|
||||
fetchurl,
|
||||
writeText,
|
||||
graphviz,
|
||||
doxygen,
|
||||
ocamlPackages,
|
||||
ltl2ba,
|
||||
coq,
|
||||
dune,
|
||||
why3,
|
||||
gdk-pixbuf,
|
||||
wrapGAppsHook3,
|
||||
}:
|
||||
|
||||
let
|
||||
mkocamlpath = p: "${p}/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib";
|
||||
runtimeDeps = with ocamlPackages; [
|
||||
apron.dev
|
||||
bigarray-compat
|
||||
biniou
|
||||
camlzip
|
||||
easy-format
|
||||
menhirLib
|
||||
mlgmpidl
|
||||
num
|
||||
ocamlgraph
|
||||
ppx_deriving
|
||||
ppx_deriving_yojson
|
||||
ppx_import
|
||||
stdlib-shims
|
||||
why3.dev
|
||||
re
|
||||
result
|
||||
seq
|
||||
sexplib
|
||||
sexplib0
|
||||
parsexp
|
||||
base
|
||||
unionFind
|
||||
yojson
|
||||
zarith
|
||||
];
|
||||
ocamlpath = lib.concatMapStringsSep ":" mkocamlpath runtimeDeps;
|
||||
in
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
pname = "frama-c";
|
||||
version = "31.0";
|
||||
slang = "Gallium";
|
||||
|
||||
src = fetchurl {
|
||||
url = "https://frama-c.com/download/frama-c-${version}-${slang}.tar.gz";
|
||||
hash = "sha256-qUOE8A1TeRy7S02Dq0Fge8cZYtQkYfAtcRFsT/bcpWc=";
|
||||
};
|
||||
|
||||
preConfigure = ''
|
||||
substituteInPlace src/dune --replace-warn " bytes " " "
|
||||
'';
|
||||
|
||||
postConfigure = "patchShebangs ivette/api.sh";
|
||||
|
||||
strictDeps = true;
|
||||
|
||||
nativeBuildInputs = [
|
||||
wrapGAppsHook3
|
||||
dune
|
||||
]
|
||||
++ (with ocamlPackages; [
|
||||
ocaml
|
||||
findlib
|
||||
menhir
|
||||
]);
|
||||
|
||||
buildInputs = with ocamlPackages; [
|
||||
camlzip
|
||||
dune-site
|
||||
dune-configurator
|
||||
ocamlgraph
|
||||
yojson
|
||||
menhirLib
|
||||
lablgtk3
|
||||
lablgtk3-sourceview3
|
||||
coq
|
||||
graphviz
|
||||
zarith
|
||||
apron
|
||||
why3
|
||||
mlgmpidl
|
||||
doxygen
|
||||
ppx_deriving
|
||||
ppx_deriving_yaml
|
||||
ppx_deriving_yojson
|
||||
gdk-pixbuf
|
||||
unionFind
|
||||
];
|
||||
|
||||
buildPhase = ''
|
||||
runHook preBuild
|
||||
dune build -j$NIX_BUILD_CORES --release @install
|
||||
runHook postBuild
|
||||
'';
|
||||
|
||||
installFlags = [ "PREFIX=$(out)" ];
|
||||
|
||||
preFixup = ''
|
||||
gappsWrapperArgs+=(--prefix OCAMLPATH ':' ${ocamlpath}:$out/lib/)
|
||||
'';
|
||||
|
||||
# Allow loading of external Frama-C plugins
|
||||
setupHook = writeText "setupHook.sh" ''
|
||||
addFramaCPath () {
|
||||
if test -d "''$1/lib/frama-c/plugins"; then
|
||||
export FRAMAC_PLUGIN="''${FRAMAC_PLUGIN-}''${FRAMAC_PLUGIN:+:}''$1/lib/frama-c/plugins"
|
||||
export OCAMLPATH="''${OCAMLPATH-}''${OCAMLPATH:+:}''$1/lib/frama-c/plugins"
|
||||
fi
|
||||
|
||||
if test -d "''$1/lib/frama-c"; then
|
||||
export OCAMLPATH="''${OCAMLPATH-}''${OCAMLPATH:+:}''$1/lib/frama-c"
|
||||
fi
|
||||
|
||||
if test -d "''$1/share/frama-c/"; then
|
||||
export FRAMAC_EXTRA_SHARE="''${FRAMAC_EXTRA_SHARE-}''${FRAMAC_EXTRA_SHARE:+:}''$1/share/frama-c"
|
||||
fi
|
||||
|
||||
}
|
||||
|
||||
addEnvHooks "$targetOffset" addFramaCPath
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Extensible and collaborative platform dedicated to source-code analysis of C software";
|
||||
homepage = "http://frama-c.com/";
|
||||
license = lib.licenses.lgpl21;
|
||||
maintainers = with lib.maintainers; [
|
||||
thoughtpolice
|
||||
amiddelk
|
||||
];
|
||||
platforms = lib.platforms.unix;
|
||||
broken = !lib.versionAtLeast ocamlPackages.ocaml.version "4.14";
|
||||
};
|
||||
}
|
||||
@@ -3,20 +3,22 @@
|
||||
pkgs,
|
||||
ocaml,
|
||||
findlib,
|
||||
framac,
|
||||
frama-c,
|
||||
camlzip,
|
||||
dune-site,
|
||||
ocamlgraph,
|
||||
menhirLib,
|
||||
ppx_deriving,
|
||||
ppx_inline_test,
|
||||
yaml,
|
||||
yojson,
|
||||
zarith,
|
||||
zmq,
|
||||
}:
|
||||
|
||||
stdenv.mkDerivation {
|
||||
pname = "ocaml${ocaml.version}-frama-c";
|
||||
inherit (framac) version meta;
|
||||
inherit (frama-c) version meta;
|
||||
|
||||
dontUnpack = true;
|
||||
|
||||
@@ -28,15 +30,17 @@ stdenv.mkDerivation {
|
||||
menhirLib
|
||||
ocamlgraph
|
||||
ppx_deriving
|
||||
ppx_inline_test
|
||||
yaml
|
||||
yojson
|
||||
zarith
|
||||
zmq
|
||||
];
|
||||
|
||||
installPhase = ''
|
||||
runHook preInstall
|
||||
mkdir -p $OCAMLFIND_DESTDIR
|
||||
for p in ${framac}/lib/*
|
||||
for p in ${frama-c}/lib/*
|
||||
do
|
||||
ln -s $p $OCAMLFIND_DESTDIR/
|
||||
done
|
||||
|
||||
@@ -783,6 +783,7 @@ mapAliases {
|
||||
forge = throw "forge was removed due to numerous vulnerabilities in freeimage"; # Added 2025-10-23
|
||||
forgejo-actions-runner = throw "'forgejo-actions-runner' has been renamed to/replaced by 'forgejo-runner'"; # Converted to throw 2025-10-27
|
||||
fractal-next = throw "'fractal-next' has been renamed to/replaced by 'fractal'"; # Converted to throw 2025-10-27
|
||||
framac = frama-c; # Added 2026-04-24
|
||||
framework-system-tools = throw "'framework-system-tools' has been renamed to/replaced by 'framework-tool'"; # Converted to throw 2025-10-27
|
||||
francis = throw "'francis' has been renamed to/replaced by 'kdePackages.francis'"; # Converted to throw 2025-10-27
|
||||
freebsdCross = throw "'freebsdCross' has been renamed to/replaced by 'freebsd'"; # Converted to throw 2025-10-27
|
||||
|
||||
@@ -676,7 +676,7 @@ let
|
||||
fpath = callPackage ../development/ocaml-modules/fpath { };
|
||||
|
||||
frama-c = callPackage ../development/ocaml-modules/frama-c {
|
||||
framac = pkgs.framac.override {
|
||||
frama-c = pkgs.frama-c.override {
|
||||
ocamlPackages = self;
|
||||
why3 = pkgs.why3.override { ocamlPackages = self; };
|
||||
};
|
||||
|
||||
Reference in New Issue
Block a user