136 lines
3.1 KiB
Nix
136 lines
3.1 KiB
Nix
{
|
|
lib,
|
|
stdenv,
|
|
fetchFromGitHub,
|
|
testers,
|
|
bison,
|
|
cadical,
|
|
cbmc,
|
|
cmake,
|
|
flex,
|
|
makeWrapper,
|
|
perl,
|
|
substituteAll,
|
|
substitute,
|
|
cudd,
|
|
fetchurl,
|
|
nix-update-script,
|
|
apple-sdk,
|
|
apple-sdk_10_15,
|
|
darwinMinVersionHook,
|
|
}:
|
|
|
|
stdenv.mkDerivation (finalAttrs: {
|
|
pname = "cbmc";
|
|
version = "6.4.0";
|
|
|
|
src = fetchFromGitHub {
|
|
owner = "diffblue";
|
|
repo = "cbmc";
|
|
rev = "refs/tags/cbmc-${finalAttrs.version}";
|
|
hash = "sha256-PZZnseOE3nodE0zwyG+82gm55BO4rsCcP4T+fZq7L6I=";
|
|
};
|
|
|
|
srcglucose = fetchFromGitHub {
|
|
owner = "brunodutertre";
|
|
repo = "glucose-syrup";
|
|
rev = "0bb2afd3b9baace6981cbb8b4a1c7683c44968b7";
|
|
hash = "sha256-+KrnXEJe7ApSuj936T615DaXOV+C2LlRxc213fQI+Q4=";
|
|
};
|
|
|
|
srccadical =
|
|
(cadical.override {
|
|
version = "2.0.0";
|
|
}).src;
|
|
|
|
nativeBuildInputs = [
|
|
bison
|
|
cmake
|
|
flex
|
|
perl
|
|
makeWrapper
|
|
];
|
|
|
|
buildInputs =
|
|
[ cadical ]
|
|
++ lib.optionals stdenv.hostPlatform.isDarwin [
|
|
(darwinMinVersionHook "10.15")
|
|
]
|
|
++ lib.optionals (stdenv.hostPlatform.isDarwin && lib.versionOlder apple-sdk.version "10.15") [
|
|
apple-sdk_10_15
|
|
];
|
|
|
|
# do not download sources
|
|
# link existing cadical instead
|
|
patches = [
|
|
(substituteAll {
|
|
src = ./0001-Do-not-download-sources-in-cmake.patch;
|
|
inherit cudd;
|
|
})
|
|
./0002-Do-not-download-sources-in-cmake.patch
|
|
];
|
|
|
|
postPatch =
|
|
''
|
|
# fix library_check.sh interpreter error
|
|
patchShebangs .
|
|
|
|
mkdir -p srccadical
|
|
cp -r ${finalAttrs.srccadical}/* srccadical
|
|
|
|
mkdir -p srcglucose
|
|
cp -r ${finalAttrs.srcglucose}/* srcglucose
|
|
find -exec chmod +w {} \;
|
|
|
|
substituteInPlace src/solvers/CMakeLists.txt \
|
|
--replace-fail "@srccadical@" "$PWD/srccadical" \
|
|
--replace-fail "@srcglucose@" "$PWD/srcglucose"
|
|
''
|
|
+ lib.optionalString (!stdenv.cc.isGNU) ''
|
|
# goto-gcc rely on gcc
|
|
substituteInPlace "regression/CMakeLists.txt" \
|
|
--replace-fail "add_subdirectory(goto-gcc)" ""
|
|
'';
|
|
|
|
postInstall = ''
|
|
# goto-cc expects ls_parse.py in PATH
|
|
mkdir -p $out/share/cbmc
|
|
mv $out/bin/ls_parse.py $out/share/cbmc/ls_parse.py
|
|
chmod +x $out/share/cbmc/ls_parse.py
|
|
wrapProgram $out/bin/goto-cc \
|
|
--prefix PATH : "$out/share/cbmc" \
|
|
'';
|
|
|
|
env.NIX_CFLAGS_COMPILE = toString (
|
|
lib.optionals stdenv.cc.isGNU [
|
|
# Needed with GCC 12 but breaks on darwin (with clang)
|
|
"-Wno-error=maybe-uninitialized"
|
|
]
|
|
++ lib.optionals stdenv.cc.isClang [
|
|
# fix "argument unused during compilation"
|
|
"-Wno-unused-command-line-argument"
|
|
]
|
|
);
|
|
|
|
# TODO: add jbmc support
|
|
cmakeFlags = [
|
|
"-DWITH_JBMC=OFF"
|
|
"-Dsat_impl=cadical"
|
|
"-Dcadical_INCLUDE_DIR=${cadical.dev}/include"
|
|
];
|
|
|
|
passthru.tests.version = testers.testVersion {
|
|
package = cbmc;
|
|
command = "cbmc --version";
|
|
};
|
|
|
|
passthru.updateScript = nix-update-script { };
|
|
|
|
meta = {
|
|
description = "CBMC is a Bounded Model Checker for C and C++ programs";
|
|
homepage = "http://www.cprover.org/cbmc/";
|
|
license = lib.licenses.bsdOriginal;
|
|
maintainers = with lib.maintainers; [ jiegec ];
|
|
platforms = lib.platforms.unix;
|
|
};
|
|
})
|