mirror of
https://github.com/NixOS/nixpkgs.git
synced 2024-09-29 07:32:58 +00:00
e0464e4788
In preparation for the deprecation of `stdenv.isX`. These shorthands are not conducive to cross-compilation because they hide the platforms. Darwin might get cross-compilation for which the continued usage of `stdenv.isDarwin` will get in the way One example of why this is bad and especially affects compiler packages https://www.github.com/NixOS/nixpkgs/pull/343059 There are too many files to go through manually but a treewide should get users thinking when they see a `hostPlatform.isX` in a place where it doesn't make sense. ``` fd --type f "\.nix" | xargs sd --fixed-strings "stdenv.is" "stdenv.hostPlatform.is" fd --type f "\.nix" | xargs sd --fixed-strings "stdenv'.is" "stdenv'.hostPlatform.is" fd --type f "\.nix" | xargs sd --fixed-strings "clangStdenv.is" "clangStdenv.hostPlatform.is" fd --type f "\.nix" | xargs sd --fixed-strings "gccStdenv.is" "gccStdenv.hostPlatform.is" fd --type f "\.nix" | xargs sd --fixed-strings "stdenvNoCC.is" "stdenvNoCC.hostPlatform.is" fd --type f "\.nix" | xargs sd --fixed-strings "inherit (stdenv) is" "inherit (stdenv.hostPlatform) is" fd --type f "\.nix" | xargs sd --fixed-strings "buildStdenv.is" "buildStdenv.hostPlatform.is" fd --type f "\.nix" | xargs sd --fixed-strings "effectiveStdenv.is" "effectiveStdenv.hostPlatform.is" fd --type f "\.nix" | xargs sd --fixed-strings "originalStdenv.is" "originalStdenv.hostPlatform.is" ```
89 lines
2.2 KiB
Nix
89 lines
2.2 KiB
Nix
{ lib
|
|
, stdenv
|
|
, fetchFromGitHub
|
|
, testers
|
|
, bison
|
|
, cadical
|
|
, cbmc
|
|
, cmake
|
|
, flex
|
|
, makeWrapper
|
|
, perl
|
|
}:
|
|
|
|
stdenv.mkDerivation rec {
|
|
pname = "cbmc";
|
|
version = "6.0.1";
|
|
|
|
src = fetchFromGitHub {
|
|
owner = "diffblue";
|
|
repo = pname;
|
|
rev = "${pname}-${version}";
|
|
sha256 = "sha256-7syRpCNL7TRZoJaNrmAdahNy7IyovyniYyOwD/lzhuw=";
|
|
};
|
|
|
|
nativeBuildInputs = [
|
|
bison
|
|
cmake
|
|
flex
|
|
perl
|
|
makeWrapper
|
|
];
|
|
|
|
buildInputs = [ cadical ];
|
|
|
|
# do not download sources
|
|
# link existing cadical instead
|
|
patches = [
|
|
./0001-Do-not-download-sources-in-cmake.patch
|
|
];
|
|
|
|
postPatch = ''
|
|
# do not hardcode gcc
|
|
substituteInPlace "scripts/bash-autocomplete/extract_switches.sh" \
|
|
--replace "gcc" "$CC" \
|
|
--replace "g++" "$CXX"
|
|
# fix library_check.sh interpreter error
|
|
patchShebangs .
|
|
'' + lib.optionalString (!stdenv.cc.isGNU) ''
|
|
# goto-gcc rely on gcc
|
|
substituteInPlace "regression/CMakeLists.txt" \
|
|
--replace "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";
|
|
};
|
|
|
|
meta = with lib; {
|
|
description = "CBMC is a Bounded Model Checker for C and C++ programs";
|
|
homepage = "http://www.cprover.org/cbmc/";
|
|
license = licenses.bsdOriginal;
|
|
maintainers = with maintainers; [ jiegec ];
|
|
platforms = platforms.unix;
|
|
# error: no member named 'aligned_alloc' in the global namespace
|
|
broken = stdenv.hostPlatform.isDarwin && stdenv.hostPlatform.isx86_64;
|
|
};
|
|
}
|