frama-c: 31.0 -> 32.1 (#512924)

This commit is contained in:
Vincent Laporte
2026-05-20 09:53:06 +00:00
committed by GitHub
9 changed files with 302 additions and 154 deletions

View File

@@ -16075,6 +16075,12 @@
githubId = 83420438;
name = "Lewis";
};
luc65r = {
email = "lucas@ransan.fr";
github = "luc65r";
githubId = 59375051;
name = "Lucas Ransan";
};
LucaGuerra = {
email = "luca@guerra.sh";
github = "LucaGuerra";

View File

@@ -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";
};
})

View File

@@ -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";
};
}

View File

@@ -0,0 +1,137 @@
{
lib,
stdenv,
fetchzip,
fetchYarnDeps,
yarn,
fixup-yarn-lock,
yarnConfigHook,
nodejs_22,
electron,
frama-c,
makeWrapper,
makeBinaryWrapper,
makeDesktopItem,
}:
stdenv.mkDerivation (finalAttrs: {
pname = "ivette";
version = "32.1";
slang = "Germanium";
__structuredAttrs = true;
# Not fetchurl, because we need it unzipped before fetchYarnDeps
src = fetchzip {
url = "https://frama-c.com/download/frama-c-${finalAttrs.version}-${finalAttrs.slang}.tar.gz";
hash = "sha256-D+OJy/pcOqSSexqHVsyCSLSHcMg8zbjKDfmqBZ8xvbk=";
};
sourceRoot = "${finalAttrs.src.name}/ivette";
yarnOfflineCache = fetchYarnDeps {
yarnLock = "${finalAttrs.src}/ivette/yarn.lock";
hash = "sha256-1NRSTJkXZ1jvkB/7xI0+u4PmrEzKc3VVBdwM50PtznI=";
};
env.ELECTRON_SKIP_BINARY_DOWNLOAD = "1";
strictDeps = true;
nativeBuildInputs = [
yarnConfigHook
nodejs_22
yarn
]
++ lib.optionals stdenv.hostPlatform.isLinux [
makeWrapper
]
++ lib.optionals stdenv.hostPlatform.isDarwin [
makeBinaryWrapper
];
postPatch = ''
substituteInPlace src/frama-c/server.ts \
--replace-fail "command = 'frama-c'" \
"command = '${lib.getExe frama-c}'"
'';
buildPhase = ''
runHook preBuild
# From api.sh
${lib.getExe frama-c} -server-tsc -server-tsc-out src
# Run configure.js and sandboxer.js
make pkg
# From src/dome/template/makefile:103
cp ./src/dome/template/react-virtualized.hacked.onScroll.js \
./node_modules/react-virtualized/dist/es/WindowScroller/utils/onScroll.js
DOME=./src/dome DOME_ENV=app yarn --offline run build
# Workaround for Darwin
cp -r ${electron.dist} electron-dist
chmod -R u+w electron-dist
yarn --offline electron-builder --dir \
-c.electronDist=electron-dist \
-c.electronVersion=${electron.version}
runHook postBuild
'';
installPhase = ''
runHook preInstall
''
+ lib.optionalString stdenv.hostPlatform.isLinux ''
mkdir -p "$out/share/lib/ivette"
cp -r dist/*-unpacked/{locales,resources{,.pak}} "$out/share/lib/ivette"
install -Dm444 static/icon.png $out/share/icons/hicolor/512x512/apps/ivette.png
makeWrapper '${electron}/bin/electron' "$out/bin/ivette" \
--add-flags "$out/share/lib/ivette/resources/app.asar" \
--add-flags "\''${NIXOS_OZONE_WL:+\''${WAYLAND_DISPLAY:+--ozone-platform-hint=auto --enable-features=WaylandWindowDecorations --enable-wayland-ime=true}}" \
--add-flags "--no-sandbox" \
--inherit-argv0
''
+ lib.optionalString stdenv.hostPlatform.isDarwin ''
mkdir -p $out/Applications
cp -r dist/mac*/Ivette.app "$out/Applications/Ivette.app"
makeWrapper "$out/Applications/Ivette.app/Contents/MacOS/Ivette" "$out/bin/ivette"
''
+ ''
runHook postInstall
'';
desktopItems = lib.optional stdenv.hostPlatform.isLinux (makeDesktopItem {
name = "ivette";
exec = "ivette";
icon = "ivette";
desktopName = "Ivette";
genericName = "Frama-C's GUI";
comment = finalAttrs.meta.description;
categories = [ "Development" ];
startupWMClass = "Ivette";
});
meta = {
description = "Graphical User Interface for Frama-C";
longDescription = ''
Ivette is the Graphical User Interface (GUI) of Frama-C. It
enables exploring code, augmented with several navigation tools
and highlighting modes; it allows launching, parametrizing and
visualizing analyses; and it allows combining them seamlessly,
taking full advantage of the multi-paradigm approach.
'';
homepage = "https://www.frama-c.com/html/ivette.html";
license = lib.licenses.lgpl21;
maintainers = with lib.maintainers; [
luc65r
];
platforms = lib.platforms.unix;
mainProgram = "ivette";
};
})

View File

@@ -8,11 +8,11 @@
buildDunePackage (finalAttrs: {
pname = "frama-c-lannotate";
version = "0.2.4";
version = "0.2.5";
src = fetchzip {
url = "https://git.frama-c.com/pub/ltest/lannotate/-/archive/${finalAttrs.version}/lannotate-${finalAttrs.version}.tar.bz2";
hash = "sha256-JoD2M3R3/DcUMt33QOvwqHg4eToCgjB8riKc09TWdyc=";
hash = "sha256-S7/So+1HBdkeq4k7BisEe2gpzW4vHFi6x8J8evaPgRw=";
};
propagatedBuildInputs = [

View File

@@ -2,7 +2,7 @@
lib,
buildDunePackage,
dune-site,
fetchzip,
fetchFromGitLab,
frama-c,
menhir,
unionFind,
@@ -11,11 +11,15 @@
buildDunePackage (finalAttrs: {
pname = "frama-c-luncov";
version = "0.2.4";
version = "0.2.4-unstable-2025-11-24";
src = fetchzip {
url = "https://git.frama-c.com/pub/ltest/luncov/-/archive/${finalAttrs.version}/luncov-${finalAttrs.version}.tar.bz2";
hash = "sha256-E7zzm9qs34V+sRHElpe1JKHjeyXGALXVj1DNMVzlWn0=";
src = fetchFromGitLab {
group = "pub";
owner = "ltest";
repo = "luncov";
domain = "git.frama-c.com";
rev = "76b14a41ae9e5eacb90649cb1401a75e37a61d52"; # latest commit from stable/germanium branch
hash = "sha256-dp693isevR4N4V/3FZ1lnbw0xjR+CuAK8BD/Bwvny0E";
};
nativeBuildInputs = [

View File

@@ -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

View File

@@ -793,6 +793,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

View File

@@ -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; };
};